let a, b be real number ; :: thesis: abs a <= sqrt ((a ^2) + (b ^2))
b ^2 >= 0 by XREAL_1:65;
then ( a ^2 >= 0 & (a ^2) + 0 <= (a ^2) + (b ^2) ) by XREAL_1:8, XREAL_1:65;
then sqrt (a ^2) <= sqrt ((a ^2) + (b ^2)) by SQUARE_1:94;
hence abs a <= sqrt ((a ^2) + (b ^2)) by Lm24; :: thesis: verum