Let x be given.

Assume Hx: x ∈ X ∖ (A ∩ B).

We will prove x ∈ (X ∖ A) ∪ (X ∖ B).

We prove the intermediate claim Hxpair: x ∈ X ∧ x ∉ (A ∩ B).

An exact proof term for the current goal is (setminusE X (A ∩ B) x Hx).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (x ∉ (A ∩ B)) Hxpair).

We prove the intermediate claim HxNotAB: x ∉ (A ∩ B).

An exact proof term for the current goal is (andER (x ∈ X) (x ∉ (A ∩ B)) Hxpair).

Apply (xm (x ∈ A)) to the current goal.

Assume HxA: x ∈ A.

We prove the intermediate claim HxNotB: x ∉ B.

Assume HxB: x ∈ B.

We prove the intermediate claim HxAB: x ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B x HxA HxB).

An exact proof term for the current goal is (HxNotAB HxAB).

An exact proof term for the current goal is (binunionI2 (X ∖ A) (X ∖ B) x (setminusI X B x HxX HxNotB)).

Assume HxNotA: ¬ (x ∈ A).

An exact proof term for the current goal is (binunionI1 (X ∖ A) (X ∖ B) x (setminusI X A x HxX HxNotA)).

Let x be given.

Assume Hx: x ∈ (X ∖ A) ∪ (X ∖ B).

We will prove x ∈ X ∖ (A ∩ B).

Apply (binunionE (X ∖ A) (X ∖ B) x Hx) to the current goal.

Assume HxXA: x ∈ X ∖ A.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (setminusE1 X A x HxXA).

We prove the intermediate claim HxNotAB: x ∉ A ∩ B.

Assume HxAB: x ∈ A ∩ B.

We prove the intermediate claim HxA: x ∈ A.

An exact proof term for the current goal is (binintersectE1 A B x HxAB).

An exact proof term for the current goal is ((setminusE2 X A x HxXA) HxA).

An exact proof term for the current goal is (setminusI X (A ∩ B) x HxX HxNotAB).

Assume HxXB: x ∈ X ∖ B.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (setminusE1 X B x HxXB).

We prove the intermediate claim HxNotAB: x ∉ A ∩ B.

Assume HxAB: x ∈ A ∩ B.

We prove the intermediate claim HxB: x ∈ B.

An exact proof term for the current goal is (binintersectE2 A B x HxAB).

An exact proof term for the current goal is ((setminusE2 X B x HxXB) HxB).

An exact proof term for the current goal is (setminusI X (A ∩ B) x HxX HxNotAB).