theorem :: SQUARE_1:27

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