Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply dneg with
∃ x3 . and (x3 ∈ x1) (SNoLe x3 x2).
Apply H0 with
False.
Assume H3:
and (∀ x3 . x3 ∈ x0 ⟶ SNo x3) (∀ x3 . x3 ∈ x1 ⟶ SNo x3).
Apply H3 with
(∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ SNoLt x3 x4) ⟶ False.
Assume H4:
∀ x3 . x3 ∈ x0 ⟶ SNo x3.
Assume H5:
∀ x3 . x3 ∈ x1 ⟶ SNo x3.
Assume H6:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ SNoLt x3 x4.
Apply SNoCutP_SNoCut_impred with
x0,
x1,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoR_E with
SNoCut x0 x1,
x2,
False leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H1.
Apply In_irref with
SNoLev x2.
Apply andEL with
SNoLev (SNoCut x0 x1) ⊆ SNoLev x2,
SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2,
SNoLev x2 leaving 2 subgoals.
Apply H11 with
x2 leaving 3 subgoals.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Assume H15: x3 ∈ x0.
Apply SNoLt_tra with
x3,
SNoCut x0 x1,
x2 leaving 5 subgoals.
Apply H4 with
x3.
The subproof is completed by applying H15.
The subproof is completed by applying H7.
The subproof is completed by applying H12.
Apply H9 with
x3.
The subproof is completed by applying H15.
The subproof is completed by applying H14.
Let x3 of type ι be given.
Assume H15: x3 ∈ x1.
Apply SNoLtLe_or with
x2,
x3,
SNoLt x2 x3 leaving 4 subgoals.
The subproof is completed by applying H12.
Apply H5 with
x3.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply H2 with
SNoLt x2 x3.
Let x4 of type ο be given.
Assume H17:
∀ x5 . and (x5 ∈ x1) (SNoLe x5 x2) ⟶ x4.
Apply H17 with
x3.
Apply andI with
x3 ∈ x1,
SNoLe x3 x2 leaving 2 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
The subproof is completed by applying H13.