Let X, Tx, x and y be given.
Assume H: path_connected_space X Tx.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
We prove the intermediate claim Hpaths: ∀x0 y0 : set, x0 ∈ X → y0 ∈ X → ∃p : set, path_between X x0 y0 p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 y0 : set, x0 ∈ X → y0 ∈ X → ∃p : set, path_between X x0 y0 p ∧ continuous_map unit_interval unit_interval_topology X Tx p) H).
An exact proof term for the current goal is (Hpaths x y Hx Hy).
∎