Let x0 of type ι be given.
Apply dneg with
∃ x1 . x1 ∈ x0.
Assume H1:
not (∃ x1 . x1 ∈ x0).
Apply H0.
Let x1 of type ι be given.
Assume H2: x1 ∈ x0.
Apply H1.
Let x2 of type ο be given.
Assume H3: ∀ x3 . x3 ∈ x0 ⟶ x2.
Apply H3 with
x1.
The subproof is completed by applying H2.