:: deftheorem Def7 defines eLoop BORSUK_7:def 7 :
for r being Real
for b₂ being Function of I[01],(Tunit_circle 3) holds
( b₂ = eLoop r iff for x being Point of I[01] holds b₂ . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| );