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