for x being Point of I[01] holds (1 / 2) * x is Point of I[01]