let a, b be real positive number ; :: 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:8;
then (((a ^2 ) + (b ^2 )) + (((a ^2 ) + (b ^2 )) / 2)) / 3 >= (((a ^2 ) + (a * b)) + (b ^2 )) / 3 by XREAL_1:74;
hence sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3) <= sqrt (((a ^2 ) + (b ^2 )) / 2) by SQUARE_1:94; :: thesis: verum