Let X, Tx, net, J, le and x be given.
Assume H: accumulation_point_of_net_on X Tx net J le x.
We will prove accumulation_point_of_net X Tx net x.
We will prove ∃J0 le0 : set, topology_on X Tx ∧ directed_set J0 le0 ∧ total_function_on net J0 X ∧ functional_graph net ∧ graph_domain_subset net J0 ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J0 → ∃j : set, j ∈ J0 ∧ (j0,j) ∈ le0 ∧ apply_fun net j ∈ U.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
An exact proof term for the current goal is H.
∎