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