let a, b, c be real positive number ; ((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 )))
A1:
(sqrt (((a ^2 ) + (b ^2 )) / 2)) ^2 = ((a ^2 ) + (b ^2 )) / 2
by SQUARE_1:def 4;
A2:
(sqrt (((b ^2 ) + (c ^2 )) / 2)) ^2 = ((b ^2 ) + (c ^2 )) / 2
by SQUARE_1:def 4;
A3:
sqrt (((c ^2 ) + (a ^2 )) / 2) > 0
by SQUARE_1:93;
A4:
sqrt (((b ^2 ) + (c ^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))) ^2 >= 0
by XREAL_1:65;
A6:
sqrt (((a ^2 ) + (b ^2 )) / 2) > 0
by SQUARE_1:93;
A7:
(sqrt (((c ^2 ) + (a ^2 )) / 2)) ^2 = ((c ^2 ) + (a ^2 )) / 2
by SQUARE_1:def 4;
(((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;
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 A1, A2, A7, A5, 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 A6, A4, A3, SQUARE_1:89; verum