Let X, Tx, A and x be given.
Assume Htop: topology_on X Tx.
Assume HA: A ⊆ X.
Assume HxX: x ∈ X.
Assume Hxnotcl: x ∉ closure_of X Tx A.
We will prove ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ∩ A = Empty.
Apply (xm (∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ∩ A = Empty)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hnoex: ¬ (∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ∩ A = Empty).
Apply FalseE to the current goal.
Apply Hxnotcl to the current goal.
We will prove x ∈ closure_of X Tx A.
We will prove x ∈ {y ∈ X|∀U : set, U ∈ Tx → y ∈ U → U ∩ A ≠ Empty}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove ∀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 Heq: U ∩ A = Empty.
Apply Hnoex to the current goal.
We use U to witness the existential quantifier.
We will prove U ∈ Tx ∧ x ∈ U ∧ U ∩ A = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is Heq.
∎