Let x0 of type ι be given.
Apply minus_SNo_In with
omega,
x0 leaving 3 subgoals.
The subproof is completed by applying SNo_omega.
Apply ordinal_SNoLev with
omega,
λ x1 x2 . x0 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
The subproof is completed by applying H0.