An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → ∀U : set, U ∈ Tx → x ∈ U → ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ U ∧ path_connected_space V (subspace_topology X Tx V)) H).