let a, b be positive Real; :: 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 ((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:6;
then sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)) >= sqrt ((3 * ((a ^2) + (b ^2))) + ((6 * a) * b)) by SQUARE_1:26;
then A1: (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:64;
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:29
.= (sqrt 3) * (a + b) by SQUARE_1:22 ;
hence sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b) by A1, Lm10; :: thesis: verum