Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply not_and_or_demorgan with
x2 ∈ x0,
x2 ∈ x1.
Assume H1:
and (x2 ∈ x0) (x2 ∈ x1).
Apply H1 with
False.
Assume H2: x2 ∈ x0.
Assume H3: x2 ∈ x1.
Apply H0.
Apply binintersectI with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.