Let α be given.

Assume Ha: ordinal α.

We will prove α ⊆ SNoElts_ α ∧ ∀β ∈ α, exactly1of2 (β ' ∈ α) (β ∈ α).

Apply andI to the current goal.

We will prove α ⊆ SNoElts_ α.

Let β be given.

Assume Hb: β ∈ α.

We will prove β ∈ α ∪ {β '|β ∈ α}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hb.

We will prove ∀β ∈ α, exactly1of2 (β ' ∈ α) (β ∈ α).

Let β be given.

Assume Hb: β ∈ α.

Apply exactly1of2_I2 to the current goal.

We will prove β ' ∉ α.

Assume H1: β ' ∈ α.

We will prove False.

Apply tagged_not_ordinal β to the current goal.

We will prove ordinal (β ').

An exact proof term for the current goal is ordinal_Hered α Ha (β ') H1.

We will prove β ∈ α.

An exact proof term for the current goal is Hb.

∎