Let A, X, Tx and U be given.
Assume HTx: topology_on X Tx.
Assume Hdense: closure_of X Tx A = X.
Assume HU: U ∈ Tx.
Assume HUne: U ≠ Empty.
We prove the intermediate claim Hexx: ∃x : set, x ∈ U.
An exact proof term for the current goal is (nonempty_has_element U HUne).
Apply Hexx to the current goal.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub U HU).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (PowerE X U HUpow x HxU).
We prove the intermediate claim Hcl: x ∈ closure_of X Tx A.
rewrite the current goal using Hdense (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim Hcliff: x ∈ closure_of X Tx A ↔ (∀V ∈ Tx, x ∈ V → V ∩ A ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx A x HTx HxX).
We prove the intermediate claim Hneigh: ∀V ∈ Tx, x ∈ V → V ∩ A ≠ Empty.
An exact proof term for the current goal is (iffEL (x ∈ closure_of X Tx A) (∀V ∈ Tx, x ∈ V → V ∩ A ≠ Empty) Hcliff Hcl).
An exact proof term for the current goal is (Hneigh U HU HxU).
∎