for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic