:: deftheorem Def10 defines liftPath BORSUK_7:def 10 :
for x0, y0 being Point of (Tunit_circle 2)
for xt being set
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
for b₅ being Function of I[01],R^1 holds
( b₅ = liftPath (f,xt) iff ( b₅ . 0 = xt & f = CircleMap * b₅ & b₅ is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
b₅ = f1 ) ) );