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