Let X and Tx be given.

Assume Htop: topology_on X Tx.

We will prove closure_of X Tx X = X.

Apply set_ext to the current goal.

An exact proof term for the current goal is (closure_in_space X Tx X Htop).

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

∎