let a, b, c be positive Real; ((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 2;
A2:
(sqrt (((b ^2) + (c ^2)) / 2)) ^2 = ((b ^2) + (c ^2)) / 2
by SQUARE_1:def 2;
A3:
sqrt (((c ^2) + (a ^2)) / 2) > 0
by SQUARE_1:25;
A4:
sqrt (((b ^2) + (c ^2)) / 2) > 0
by SQUARE_1:25;
A5:
(((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2))) ^2 >= 0
by XREAL_1:63;
A6:
sqrt (((a ^2) + (b ^2)) / 2) > 0
by SQUARE_1:25;
A7:
(sqrt (((c ^2) + (a ^2)) / 2)) ^2 = ((c ^2) + (a ^2)) / 2
by SQUARE_1:def 2;
(((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:26;
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:22; verum