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