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