Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H2 with
False leaving 2 subgoals.
Apply In_no2cycle with
0,
u3 leaving 2 subgoals.
The subproof is completed by applying In_0_3.
The subproof is completed by applying H3.
Assume H3:
and (u3 = 0) (x0 ∈ x1).
Apply H3 with
False.
Apply FalseE with
x0 ∈ x1 ⟶ False.
Apply In_irref with
0.
Apply H4 with
λ x2 x3 . 0 ∈ x2.
The subproof is completed by applying In_0_3.