let a, b, c be real positive number ; :: thesis: ((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2)) <= sqrt (3 * (((a ^2 ) + (b ^2 )) + (c ^2 )))
A2: ( (sqrt (((a ^2 ) + (b ^2 )) / 2)) ^2 = ((a ^2 ) + (b ^2 )) / 2 & (sqrt (((b ^2 ) + (c ^2 )) / 2)) ^2 = ((b ^2 ) + (c ^2 )) / 2 & (sqrt (((c ^2 ) + (a ^2 )) / 2)) ^2 = ((c ^2 ) + (a ^2 )) / 2 ) by SQUARE_1:def 4;
A3: (((1 * (sqrt (((a ^2 ) + (b ^2 )) / 2))) + (1 * (sqrt (((b ^2 ) + (c ^2 )) / 2)))) + (1 * (sqrt (((c ^2 ) + (a ^2 )) / 2)))) ^2 <= (((1 ^2 ) + (1 ^2 )) + (1 ^2 )) * ((((sqrt (((a ^2 ) + (b ^2 )) / 2)) ^2 ) + ((sqrt (((b ^2 ) + (c ^2 )) / 2)) ^2 )) + ((sqrt (((c ^2 ) + (a ^2 )) / 2)) ^2 )) by Th29;
A4: ( sqrt (((a ^2 ) + (b ^2 )) / 2) > 0 & sqrt (((b ^2 ) + (c ^2 )) / 2) > 0 & sqrt (((c ^2 ) + (a ^2 )) / 2) > 0 ) by SQUARE_1:93;
A5: ((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2)) > 0 by A4;
(((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2))) ^2 >= 0 by XREAL_1:65;
then sqrt ((((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2))) ^2 ) <= sqrt (3 * (((a ^2 ) + (b ^2 )) + (c ^2 ))) by A2, A3, SQUARE_1:94;
hence ((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2)) <= sqrt (3 * (((a ^2 ) + (b ^2 )) + (c ^2 ))) by A5, SQUARE_1:89; :: thesis: verum