Apply Empty_eq with
SNoS_ 0.
Let x0 of type ι be given.
Apply SNoS_E with
0,
x0,
False leaving 3 subgoals.
The subproof is completed by applying ordinal_Empty.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1:
(λ x2 . and (x2 ∈ 0) (SNo_ x2 x0)) x1.
Apply H1 with
False.
Assume H2: x1 ∈ 0.
Apply FalseE with
SNo_ x1 x0 ⟶ False.
Apply EmptyE with
x1.
The subproof is completed by applying H2.