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