:: deftheorem Def7 defines 3RP BORSUK_6:def 7 :
for b₁ being Function of I[01],I[01] holds
( b₁ = 3RP iff for x being Point of I[01] holds
( ( x <= 1 / 2 implies b₁ . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b₁ . x = x - (1 / 4) ) & ( x > 3 / 4 implies b₁ . x = (2 * x) - 1 ) ) );