:: deftheorem Def6 defines 2RP BORSUK_6:def 6 :
for b₁ being Function of I[01],I[01] holds
( b₁ = 2RP iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₁ . t = 0 ) & ( t > 1 / 2 implies b₁ . t = (2 * t) - 1 ) ) );