Let X, Tx and A be given.
Assume H: limit_point_compact X Tx.
Assume HA: A ⊆ X.
Assume Hinf: infinite A.
We prove the intermediate claim Hprop: ∀A0 : set, A0 ⊆ X → infinite A0 → ∃x : set, limit_point_of X Tx A0 x.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀A0 : set, A0 ⊆ X → infinite A0 → ∃x : set, limit_point_of X Tx A0 x) H).
An exact proof term for the current goal is (Hprop A HA Hinf).
∎