:: deftheorem defines are_homotopic BORSUK_2:def 7 :
for T being non empty TopStruct
for a, b being Point of T
for P, Q being Path of a,b holds
( P,Q are_homotopic iff ex f being Function of [:I[01],I[01]:],T st
( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ) );