Let x be given.

Assume Hx: x ∈ X ∖ (X ∖ U).

We will prove x ∈ U.

We prove the intermediate claim Hxpair: x ∈ X ∧ x ∉ (X ∖ U).

An exact proof term for the current goal is (setminusE X (X ∖ U) x Hx).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (x ∉ (X ∖ U)) Hxpair).

We prove the intermediate claim HxNot: x ∉ (X ∖ U).

An exact proof term for the current goal is (andER (x ∈ X) (x ∉ (X ∖ U)) Hxpair).

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

Assume HxU.

An exact proof term for the current goal is HxU.

Assume HxNotU: ¬ (x ∈ U).

We prove the intermediate claim HxXU: x ∈ X ∖ U.

An exact proof term for the current goal is (setminusI X U x HxX HxNotU).

An exact proof term for the current goal is (FalseE (HxNot HxXU) (x ∈ U)).

Let x be given.

Assume HxU: x ∈ U.

We will prove x ∈ X ∖ (X ∖ U).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HUsub x HxU).

We prove the intermediate claim HxNot: x ∉ (X ∖ U).

Assume HxXU: x ∈ X ∖ U.

An exact proof term for the current goal is ((setminusE2 X U x HxXU) HxU).

An exact proof term for the current goal is (setminusI X (X ∖ U) x HxX HxNot).