Let x0 of type ι be given.
Apply SNoS_E2 with
omega,
x0,
minus_SNo x0 ∈ SNoS_ omega leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Apply SNoS_I with
omega,
minus_SNo x0,
SNoLev (minus_SNo x0) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply minus_SNo_Lev with
x0,
λ x1 x2 . x2 ∈ omega leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply SNoLev_ with
minus_SNo x0.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H3.