Let x0 of type ι be given.
Let x1 of type ι be given.
Apply V_In_or_Subq with
x0,
x1,
or (V_ x0 ∈ V_ x1) (V_ x1 ⊆ V_ x0) leaving 2 subgoals.
Apply orIL with
V_ x0 ∈ V_ x1,
V_ x1 ⊆ V_ x0.
Apply V_In with
x0,
x1.
The subproof is completed by applying H0.
Assume H0:
V_ x1 ⊆ V_ x0.
Apply orIR with
V_ x0 ∈ V_ x1,
V_ x1 ⊆ V_ x0.
The subproof is completed by applying H0.