Let x0 of type ι be given.
Let x1 of type ο be given.
Apply H1 with
{x2 ∈ SNoS_ (SNoLev x0)|SNoLt x2 x0},
{x2 ∈ SNoS_ (SNoLev x0)|SNoLt x0 x2} leaving 4 subgoals.
Apply and3I with
∀ x2 . x2 ∈ {x3 ∈ SNoS_ (SNoLev x0)|SNoLt x3 x0} ⟶ SNo x2,
∀ x2 . x2 ∈ {x3 ∈ SNoS_ (SNoLev x0)|SNoLt x0 x3} ⟶ SNo x2,
∀ x2 . x2 ∈ {x3 ∈ SNoS_ (SNoLev x0)|SNoLt x3 x0} ⟶ ∀ x3 . x3 ∈ {x4 ∈ SNoS_ (SNoLev x0)|SNoLt x0 x4} ⟶ SNoLt x2 x3 leaving 3 subgoals.
Let x2 of type ι be given.
Apply L4 with
x2,
SNo x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H7 with
SNo x2.
The subproof is completed by applying H9.
Let x2 of type ι be given.
Apply L5 with
x2,
SNo x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H7 with
SNo x2.
The subproof is completed by applying H9.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply L4 with
x2,
SNoLt x2 x3 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H8 with
SNoLt x2 x0 ⟶ SNoLt x2 x3.
Apply L5 with
x3,
SNoLt x2 x3 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply H12 with
SNoLt x0 x3 ⟶ SNoLt x2 x3.
Apply SNoLt_tra with
x2,
x0,
x3 leaving 5 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H0.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
The subproof is completed by applying H15.
Let x2 of type ι be given.