Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Apply set_ext with setminus x0 (binintersect x1 x2), binunion (setminus x0 x1) (setminus x0 x2) leaving 2 subgoals.

Let x3 of type ι be given.

Assume H0: x3 ∈ setminus x0 (binintersect x1 x2).

Apply setminusE with x0, binintersect x1 x2, x3, x3 ∈ binunion (setminus x0 x1) (setminus x0 x2) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: x3 ∈ x0.

Assume H2: nIn x3 (binintersect x1 x2).

Apply dneg with x3 ∈ binunion (setminus x0 x1) (setminus x0 x2).

Assume H3: nIn x3 (binunion (setminus x0 x1) (setminus x0 x2)).

Apply H2.

Apply binintersectI with x1, x2, x3 leaving 2 subgoals.

Apply dneg with x3 ∈ x1.

Assume H4: nIn x3 x1.

Apply H3.

Apply binunionI1 with setminus x0 x1, setminus x0 x2, x3.

Apply setminusI with x0, x1, x3 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H4.

Apply dneg with x3 ∈ x2.

Assume H4: nIn x3 x2.

Apply H3.

Apply binunionI2 with setminus x0 x1, setminus x0 x2, x3.

Apply setminusI with x0, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H4.

Apply binunion_Subq_min with setminus x0 x1, setminus x0 x2, setminus x0 (binintersect x1 x2) leaving 2 subgoals.

Apply setminus_Subq_contra with x0, x1, binintersect x1 x2.

The subproof is completed by applying binintersect_Subq_1 with x1, x2.

Apply setminus_Subq_contra with x0, x2, binintersect x1 x2.

The subproof is completed by applying binintersect_Subq_2 with x1, x2.

■

Proofgold Proof