Let X, Tx and A be given.

Assume Htop: topology_on X Tx.

Assume HA: A ⊆ X.

We will prove A ⊆ closure_of X Tx A.

Let x be given.

Assume Hx: x ∈ A.

We will prove x ∈ closure_of X Tx A.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HA x Hx).

We prove the intermediate claim Hcond: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We will prove U ∩ A ≠ Empty.

Assume Hempty: U ∩ A = Empty.

We prove the intermediate claim HxUA: x ∈ U ∩ A.

An exact proof term for the current goal is (binintersectI U A x HxU Hx).

We prove the intermediate claim HxEmpty: x ∈ Empty.

rewrite the current goal using Hempty (from right to left).

An exact proof term for the current goal is HxUA.

An exact proof term for the current goal is (EmptyE x HxEmpty).

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

∎