for T being non empty TopStruct
for c being with_endpoints Curve of T
for t1, t2 being Point of T st c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected holds
( t1 = the_first_point_of c & t2 = the_last_point_of c )