let x, y, z be Real; :: thesis: ( x ^2 <= y * z implies |.x.| <= sqrt (y * z) )
A1: x ^2 >= 0 by XREAL_1:63;
assume x ^2 <= y * z ; :: thesis: |.x.| <= sqrt (y * z)
then A2: sqrt (x ^2) <= sqrt (y * z) by A1, SQUARE_1:26;

per cases ( x >= 0 or x < 0 ) ;

suppose A3: x >= 0 ; :: thesis: |.x.| <= sqrt (y * z)

then x <= sqrt (y * z) by A2, SQUARE_1:22;
hence |.x.| <= sqrt (y * z) by A3, ABSVALUE:def 1; :: thesis: verum

end;

suppose A4: x < 0 ; :: thesis: |.x.| <= sqrt (y * z)

then - x <= sqrt (y * z) by A2, SQUARE_1:23;
hence |.x.| <= sqrt (y * z) by A4, ABSVALUE:def 1; :: thesis: verum

end;

end;