let x be Point of I[01]; :: thesis: ( x >= 1 / 2 implies x - (1 / 4) is Point of I[01] )
x <= 1 by BORSUK_1:43;
then x <= 1 + (1 / 4) by XXREAL_0:2;
then A1: x - (1 / 4) <= 1 by XREAL_1:20;
assume x >= 1 / 2 ; :: thesis: x - (1 / 4) is Point of I[01]
then x >= (1 / 4) + 0 by XXREAL_0:2;
then x - (1 / 4) >= 0 by XREAL_1:19;
hence x - (1 / 4) is Point of I[01] by A1, BORSUK_1:43; :: thesis: verum