An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x y : set, x ∈ X → y ∈ X → ∃p : set, path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p) H).