Let X, Tx, A and B be given.

Assume Htop: topology_on X Tx.

Assume HAB: A ⊆ B.

Assume HB: B ⊆ X.

We will prove closure_of X Tx A ⊆ closure_of X Tx B.

An exact proof term for the current goal is (closure_monotone X Tx A B Htop HAB HB).

∎