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