let a, b be real number ; :: thesis: sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b)
A1: (sqrt ((a ^2) + (b ^2))) ^2 >= 0 by XREAL_1:65;
( a ^2 >= 0 & b ^2 >= 0 ) by XREAL_1:65;
then A2: (sqrt ((a ^2) + (b ^2))) ^2 = (a ^2) + (b ^2) by SQUARE_1:def 4;
( ((abs a) + (abs b)) ^2 = (((abs a) ^2) + ((2 * (abs a)) * (abs b))) + ((abs b) ^2) & (abs a) ^2 = a ^2 ) by Th161;
then (((abs a) + (abs b)) ^2) - ((sqrt ((a ^2) + (b ^2))) ^2) = (((a ^2) + ((2 * (abs a)) * (abs b))) + (b ^2)) - ((a ^2) + (b ^2)) by A2, Th161
.= (2 * (abs a)) * (abs b) ;
then ((abs a) + (abs b)) ^2 >= (sqrt ((a ^2) + (b ^2))) ^2 by XREAL_1:51;
then sqrt (((abs a) + (abs b)) ^2) >= sqrt ((sqrt ((a ^2) + (b ^2))) ^2) by A1, SQUARE_1:94;
hence sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b) by A2, SQUARE_1:89; :: thesis: verum