An exact proof term for the current goal is (andEL (topology_on X Tx) (∀A : set, A ⊆ X → infinite A → ∃x : set, limit_point_of X Tx A x) H).