theorem :: TOPALG_2:18

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 ConvexHomotopy (P,Q) is Homotopy of P,Q