Let alpha be given.
Assume Ha: ordinal alpha.
We will prove alpha ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ alpha) (beta ∈ alpha).
Apply andI to the current goal.
We will prove alpha ⊆ SNoElts_ alpha.
Let beta be given.
Assume Hb: beta ∈ alpha.
We will prove beta ∈ alpha ∪ {beta '|beta ∈ alpha}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hb.
We will prove ∀beta ∈ alpha, exactly1of2 (beta ' ∈ alpha) (beta ∈ alpha).
Let beta be given.
Assume Hb: beta ∈ alpha.
Apply exactly1of2_I2 to the current goal.
We will prove beta ' ∉ alpha.
Assume H1: beta ' ∈ alpha.
We will prove False.
Apply tagged_not_ordinal beta to the current goal.
We will prove ordinal (beta ').
An exact proof term for the current goal is ordinal_Hered alpha Ha (beta ') H1.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb.
∎