for T being non empty interval SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q