Let X, Tx, A and B be given.

Assume Htop: topology_on X Tx.

Assume HA: A ⊆ X.

Assume HB: B ⊆ X.

We will prove closure_of X Tx (A ∖ B) ⊆ closure_of X Tx A.

We prove the intermediate claim Hsub: A ∖ B ⊆ A.

Let x be given.

Assume Hx: x ∈ A ∖ B.

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

An exact proof term for the current goal is (closure_monotone X Tx (A ∖ B) A Htop Hsub HA).

∎