Let X, Tx and A be given.

Assume Htop: topology_on X Tx.

Assume HA: A ⊆ X.

An exact proof term for the current goal is (subset_of_closure X Tx A Htop HA).

∎