Let x0 of type ι be given.
Apply xm with
∃ x1 . x1 ∈ x0,
or (x0 = 0) (∃ x1 . x1 ∈ x0) leaving 2 subgoals.
Assume H0: ∃ x1 . x1 ∈ x0.
Apply orIR with
x0 = 0,
∃ x1 . x1 ∈ x0.
The subproof is completed by applying H0.
Assume H0:
not (∃ x1 . x1 ∈ x0).
Apply orIL with
x0 = 0,
∃ x1 . x1 ∈ x0.
Apply set_ext with
x0,
0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: x1 ∈ x0.
Apply FalseE with
x1 ∈ 0.
Apply H0.
Let x2 of type ο be given.
Assume H2: ∀ x3 . x3 ∈ x0 ⟶ x2.
Apply H2 with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying Subq_Empty with x0.