theorem :: TOPALG_1:64

for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q