Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
∀ x2 . x2 ∈ x0 ⟶ SNo x2.
Apply H1 with
SNo_max_of {minus_SNo x2|x2 ∈ x0} (minus_SNo x1).
Assume H2:
and (x1 ∈ x0) (SNo x1).
Apply H2 with
(∀ x2 . x2 ∈ x0 ⟶ SNo x2 ⟶ SNoLe x1 x2) ⟶ SNo_max_of {minus_SNo x2|x2 ∈ x0} (minus_SNo x1).
Assume H3: x1 ∈ x0.
Assume H5:
∀ x2 . x2 ∈ x0 ⟶ SNo x2 ⟶ SNoLe x1 x2.
Apply and3I with
minus_SNo x1 ∈ {minus_SNo x2|x2 ∈ x0},
SNo (minus_SNo x1),
∀ x2 . x2 ∈ {minus_SNo x3|x3 ∈ x0} ⟶ SNo x2 ⟶ SNoLe x2 (minus_SNo x1) leaving 3 subgoals.
Apply ReplI with
x0,
minus_SNo,
x1.
The subproof is completed by applying H3.
Apply SNo_minus_SNo with
x1.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply ReplE_impred with
x0,
λ x3 . minus_SNo x3,
x2,
SNoLe x2 (minus_SNo x1) leaving 2 subgoals.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H8: x3 ∈ x0.
Apply H9 with
λ x4 x5 . SNoLe x5 (minus_SNo x1).
Apply minus_SNo_Le_contra with
x1,
x3 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H0 with
x3.
The subproof is completed by applying H8.
Apply H5 with
x3 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply H0 with
x3.
The subproof is completed by applying H8.