Let x0 of type ι be given.
Apply real_E with
x0,
minus_SNo x0 ∈ real leaving 2 subgoals.
The subproof is completed by applying H0.
Apply real_I with
minus_SNo x0 leaving 4 subgoals.
Apply minus_SNo_SNoS_ with
ordsucc omega,
x0 leaving 2 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H3.
Apply SNoLt_irref with
x0.
Apply minus_SNo_invol with
x0,
λ x1 x2 . SNoLt x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H8 with
λ x1 x2 . SNoLt (minus_SNo x2) x0.
The subproof is completed by applying H4.
Apply SNoLt_irref with
x0.
Apply minus_SNo_invol with
x0,
λ x1 x2 . SNoLt x0 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H8 with
λ x1 x2 . SNoLt x0 (minus_SNo x2).
Apply minus_SNo_invol with
omega,
λ x1 x2 . SNoLt x0 x2 leaving 2 subgoals.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying H5.
Apply minus_SNo_prereal_1 with
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.