let T be non empty TopStruct ; :: thesis: for t1, t2 being Point of T
for p being Path of t1,t2 st t1,t2 are_connected holds
p is with_endpoints Curve of T
let t1, t2 be Point of T; :: thesis: for p being Path of t1,t2 st t1,t2 are_connected holds
p is with_endpoints Curve of T
let p be Path of t1,t2; :: thesis: ( t1,t2 are_connected implies p is with_endpoints Curve of T )
assume t1,t2 are_connected ; :: thesis: p is with_endpoints Curve of T
then reconsider c = p as Curve of T by Th22;
A1: [.0,1.] = dom c by BORSUK_1:40, FUNCT_2:def 1;
0 in [.0,1.] by XXREAL_1:1;
then inf (dom c) in dom c by A1, Th4;
then dom c is left_end by XXREAL_2:def 5;
then A2: c is with_first_point ;
1 in [.0,1.] by XXREAL_1:1;
then sup (dom c) in dom c by A1, Th4;
then dom c is right_end by XXREAL_2:def 6;
then c is with_last_point ;
hence p is with_endpoints Curve of T by A2; :: thesis: verum