let x, y be Real; :: thesis: ( 0 <= x & 0 <= y & x <= y ^2 implies sqrt x <= y )
assume A1: ( 0 <= x & 0 <= y & x <= y ^2 ) ; :: thesis: sqrt x <= y
then sqrt x <= sqrt (y ^2) by SQUARE_1:26;
hence sqrt x <= y by A1, SQUARE_1:22; :: thesis: verum