for T being non empty TopStruct
for c1, c2 being with_endpoints Curve of T
for a, b being Point of T
for p1, p2 being Path of a,b st c1 = p1 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )