let x be Point of I[01]; :: thesis: ( x >= 1 / 2 implies (2 * x) - 1 is Point of I[01] )
x <= 1 by BORSUK_1:43;
then 2 * x <= 2 * 1 by XREAL_1:64;
then A1: (2 * x) - 1 <= 2 - 1 by XREAL_1:9;
assume x >= 1 / 2 ; :: thesis: (2 * x) - 1 is Point of I[01]
then 2 * x >= 2 * (1 / 2) by XREAL_1:64;
then (2 * x) - 1 >= 1 - 1 by XREAL_1:9;
hence (2 * x) - 1 is Point of I[01] by A1, BORSUK_1:43; :: thesis: verum