Let x0 of type ι be given.
Apply set_ext with
setminus x0 0,
x0 leaving 2 subgoals.
The subproof is completed by applying setminus_Subq with x0, 0.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Apply setminusI with
x0,
0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying EmptyE with x1.