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