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