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