Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H0 with
x1 = x2.
Assume H2:
and (x1 ∈ x0) (SNo x1).
Apply H2 with
(∀ x3 . x3 ∈ x0 ⟶ SNo x3 ⟶ SNoLe x3 x1) ⟶ x1 = x2.
Assume H3: x1 ∈ x0.
Assume H5:
∀ x3 . x3 ∈ x0 ⟶ SNo x3 ⟶ SNoLe x3 x1.
Apply H1 with
x1 = x2.
Assume H6:
and (x2 ∈ x0) (SNo x2).
Apply H6 with
(∀ x3 . x3 ∈ x0 ⟶ SNo x3 ⟶ SNoLe x3 x2) ⟶ x1 = x2.
Assume H7: x2 ∈ x0.
Assume H9:
∀ x3 . x3 ∈ x0 ⟶ SNo x3 ⟶ SNoLe x3 x2.
Apply SNoLe_antisym with
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply H9 with
x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply H5 with
x2 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.