Let x be given.
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.