let a, b be real positive number ; :: thesis: sqrt (((a ^2 ) + (a * b)) + (b ^2 )) >= ((1 / 2) * (sqrt 3)) * (a + b)
(a ^2 ) + (b ^2 ) >= (2 * a) * b by SERIES_3:6;
then A1: ((a ^2 ) + (b ^2 )) + ((3 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)) >= ((2 * a) * b) + ((3 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)) by XREAL_1:8;
sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)) >= sqrt ((3 * ((a ^2 ) + (b ^2 ))) + ((6 * a) * b)) by A1, SQUARE_1:94;
then A2: (1 / 2) * (sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b))) >= (1 / 2) * (sqrt ((3 * ((a ^2 ) + (b ^2 ))) + ((6 * a) * b))) by XREAL_1:66;
sqrt ((3 * ((a ^2 ) + (b ^2 ))) + ((6 * a) * b)) = sqrt (3 * ((a + b) ^2 )) ;
then sqrt ((3 * ((a ^2 ) + (b ^2 ))) + ((6 * a) * b)) = (sqrt 3) * (sqrt ((a + b) ^2 )) by SQUARE_1:97
.= (sqrt 3) * (a + b) by SQUARE_1:89 ;
hence sqrt (((a ^2 ) + (a * b)) + (b ^2 )) >= ((1 / 2) * (sqrt 3)) * (a + b) by A2, Lm10; :: thesis: verum