for x, y being Point of I[01]
for P, Q being Path of x,y holds P,Q are_homotopic by Th10, Th12;