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