Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

Set p to be the term λδ ⇒ δ ∈ x ∨ δ = α of type set → prop.

We will prove α ∈ {β ∈ ordsucc α|p β} ∪ {β '|β ∈ ordsucc α, ¬ p β}.

Apply binunionI1 to the current goal.

Apply SepI to the current goal.

We will prove α ∈ ordsucc α.

Apply ordsuccI2 to the current goal.

We will prove α ∈ x ∨ α = α.

Apply orIR to the current goal.

Use reflexivity.

∎