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