for a, b being Real st a <= b holds
for x, y being Point of (Closed-Interval-TSpace (a,b))
for P, Q being Path of x,y holds P,Q are_homotopic