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