let a, b be positive Real; :: thesis: sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2)
((a ^2) + (b ^2)) / 2 >= a * b by SERIES_3:7;
then (((a ^2) + (b ^2)) / 2) + ((a ^2) + (b ^2)) >= (a * b) + ((a ^2) + (b ^2)) by XREAL_1:6;
then (((a ^2) + (b ^2)) + (((a ^2) + (b ^2)) / 2)) / 3 >= (((a ^2) + (a * b)) + (b ^2)) / 3 by XREAL_1:72;
hence sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2) by SQUARE_1:26; :: thesis: verum