let x, y be Real; :: thesis: ( x ^2 <= y implies x <= sqrt y )
assume A1: x ^2 <= y ; :: thesis: x <= sqrt y
A2: x <= |.x.| by COMPLEX1:76;
|.x.| ^2 <= y by A1, COMPLEX1:75;
then sqrt (|.x.| ^2) <= sqrt y by SQUARE_1:26;
then |.x.| <= sqrt y by COMPLEX1:46, SQUARE_1:22;
hence x <= sqrt y by A2, XXREAL_0:2; :: thesis: verum