for x, y being Real st 0 <= x & x <= y holds
x ^2 <= y ^2