Let X, Tx, net, J, le, A, x and i0 be given.
Assume Hacc: accumulation_point_of_net_on X Tx net J le x.
Assume HAsubX: A ⊆ X.
Assume Hi0: i0 ∈ J.
Assume HtailA: ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ A.
Apply (and7E (topology_on X Tx) (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) (x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) Hacc) to the current goal.
Assume HTx HdirJ Htot Hgraph Hdom HxX HaccU.
We will prove x ∈ closure_of X Tx A.
We prove the intermediate claim Hcldef: closure_of X Tx A = {x0 ∈ X|∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hcldef (from left to right).
Apply (SepI X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX) to the current goal.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ A ≠ Empty.
Apply (HaccU U HU HxU i0 Hi0) to the current goal.
Let j be given.
Assume Hjpack: j ∈ J ∧ (i0,j) ∈ le ∧ apply_fun net j ∈ U.
We prove the intermediate claim Hjleft: j ∈ J ∧ (i0,j) ∈ le.
An exact proof term for the current goal is (andEL (j ∈ J ∧ (i0,j) ∈ le) (apply_fun net j ∈ U) Hjpack).
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) ((i0,j) ∈ le) Hjleft).
We prove the intermediate claim Hjle: (i0,j) ∈ le.
An exact proof term for the current goal is (andER (j ∈ J) ((i0,j) ∈ le) Hjleft).
We prove the intermediate claim HnetjU: apply_fun net j ∈ U.
An exact proof term for the current goal is (andER (j ∈ J ∧ (i0,j) ∈ le) (apply_fun net j ∈ U) Hjpack).
We prove the intermediate claim HnetjA: apply_fun net j ∈ A.
An exact proof term for the current goal is (HtailA j HjJ Hjle).
Apply (elem_implies_nonempty (U ∩ A) (apply_fun net j)) to the current goal.
An exact proof term for the current goal is (binintersectI U A (apply_fun net j) HnetjU HnetjA).
∎