for x being Point of I[01] st x <= 1 / 2 holds
2 * x is Point of I[01]