Let X, Tx and x be given.
Assume H: locally_compact X Tx.
Assume Hx: x ∈ X.
We prove the intermediate claim Hprop: ∀x0 : set, x0 ∈ X → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U)).
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U))) H).
An exact proof term for the current goal is (Hprop x Hx).
∎