let x, y, z be real number ; :: thesis: ( x ^2 <= y * z implies abs x <= sqrt (y * z) )
assume A1: x ^2 <= y * z ; :: thesis: abs x <= sqrt (y * z)
x ^2 >= 0 by XREAL_1:65;
then A2: sqrt (x ^2 ) <= sqrt (y * z) by A1, SQUARE_1:94;

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

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

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

end;

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

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

end;

end;