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:86;
then 2 * x <= 2 * 1 by XREAL_1:66;
then A1: (2 * x) - 1 <= 2 - 1 by XREAL_1:11;
assume x >= 1 / 2 ; :: thesis: (2 * x) - 1 is Point of I[01]
then 2 * x >= 2 * (1 / 2) by XREAL_1:66;
then (2 * x) - 1 >= 1 - 1 by XREAL_1:11;
hence (2 * x) - 1 is Point of I[01] by A1, BORSUK_1:86; :: thesis: verum