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:27;
then |.x.| < sqrt y by COMPLEX1:46, SQUARE_1:22;
hence x < sqrt y by A2, XXREAL_0:2; :: thesis: verum