Let X, Tx, A and N be given.
Assume HTx: topology_on X Tx.
Assume HNopen: N ∈ Tx.
Assume HNclNe: N ∩ closure_of X Tx A ≠ Empty.
We will prove N ∩ A ≠ Empty.
We prove the intermediate claim Hexx: ∃x : set, x ∈ (N ∩ closure_of X Tx A).
An exact proof term for the current goal is (nonempty_has_element (N ∩ closure_of X Tx A) HNclNe).
Apply Hexx to the current goal.
Let x be given.
Assume Hx: x ∈ (N ∩ closure_of X Tx A).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (binintersectE1 N (closure_of X Tx A) x Hx).
We prove the intermediate claim HxClA: x ∈ closure_of X Tx A.
An exact proof term for the current goal is (binintersectE2 N (closure_of X Tx A) x Hx).
We prove the intermediate claim HclCond: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxClA).
An exact proof term for the current goal is (HclCond N HNopen HxN).
∎