for T being non empty TopStruct
for r1, r2 being Real
for t1, t2 being Point of T
for p1 being Path of t1,t2 st t1,t2 are_connected & r1 < r2 holds
p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T