Let X, Tx and A be given.

Assume Htop: topology_on X Tx.

We will prove closure_of X Tx A ⊆ X.

Let x be given.

Assume Hx: x ∈ closure_of X Tx A.

We will prove x ∈ X.

An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hx).

∎