Let x be given.
Assume Hx: SNo x.
Set alpha to be the term SNoLev x.
Set p to be the term λdelta ⇒ delta ∈ x ∨ delta = alpha of type set → prop.
We will prove alpha ∈ {beta ∈ ordsucc alpha|p beta} ∪ {beta '|beta ∈ ordsucc alpha, ¬ p beta}.
Apply binunionI1 to the current goal.
Apply SepI to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We will prove alpha ∈ x ∨ alpha = alpha.
Apply orIR to the current goal.
Use reflexivity.
∎