Let X, Tx, A and x be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
We will prove x ∈ closure_of X Tx A ↔ (∀U ∈ Tx, x ∈ U → U ∩ A ≠ Empty).
Apply iffI to the current goal.
Assume Hx: x ∈ closure_of X Tx A.
We will prove ∀U ∈ Tx, x ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
Assume Hcond: ∀U ∈ Tx, x ∈ U → U ∩ A ≠ Empty.
We will prove x ∈ closure_of X Tx A.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX Hcond).
∎