theorem Th26: :: SQUARE_1:26

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