let x be Point of I[01]; :: thesis: (1 / 2) * x is Point of I[01]
x <= 1 by BORSUK_1:43;
then (1 / 2) * x <= (1 / 2) * 1 by XREAL_1:64;
then ( x >= 0 & (1 / 2) * x <= 1 ) by BORSUK_1:43, XXREAL_0:2;
hence (1 / 2) * x is Point of I[01] by BORSUK_1:43; :: thesis: verum