let r1, r2 be real number ; :: thesis: sqrt ((r1 ^2 ) + (r2 ^2 )) <= (abs r1) + (abs r2)
A1: r1 ^2 >= 0 by XREAL_1:65;
r2 ^2 >= 0 by XREAL_1:65;
then A2: (sqrt ((r1 ^2 ) + (r2 ^2 ))) ^2 = (r1 ^2 ) + (r2 ^2 ) by SQUARE_1:def 4, A1;
A3: ((abs r1) + (abs r2)) ^2 = (((abs r1) ^2 ) + ((2 * (abs r1)) * (abs r2))) + ((abs r2) ^2 ) ;
(abs r1) ^2 = r1 ^2 by Th161;
then A4: (((abs r1) + (abs r2)) ^2 ) - ((sqrt ((r1 ^2 ) + (r2 ^2 ))) ^2 ) = (((r1 ^2 ) + ((2 * (abs r1)) * (abs r2))) + (r2 ^2 )) - ((r1 ^2 ) + (r2 ^2 )) by A2, A3, Th161
.= (2 * (abs r1)) * (abs r2) ;
A5: abs r1 >= 0 by Th132;
A7: abs r2 >= 0 by Th132;
then A8: ((abs r1) + (abs r2)) ^2 >= (sqrt ((r1 ^2 ) + (r2 ^2 ))) ^2 by A4, A5, XREAL_1:51;
(sqrt ((r1 ^2 ) + (r2 ^2 ))) ^2 >= 0 by XREAL_1:65;
then sqrt (((abs r1) + (abs r2)) ^2 ) >= sqrt ((sqrt ((r1 ^2 ) + (r2 ^2 ))) ^2 ) by A8, SQUARE_1:94;
hence sqrt ((r1 ^2 ) + (r2 ^2 )) <= (abs r1) + (abs r2) by A2, A5, A7, SQUARE_1:89; :: thesis: verum