for x being Point of I[01] st x >= 1 / 2 holds
x - (1 / 4) is Point of I[01]