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