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:27;
hence sqrt x < y by A1, SQUARE_1:22; :: thesis: verum