let a, b, c, d, e, f be real number ; :: thesis: (((2 * (a * d)) * (c * b)) + ((2 * (a * f)) * (e * c))) + ((2 * (b * f)) * (e * d)) <= ((((((a * d) ^2 ) + ((c * b) ^2 )) + ((a * f) ^2 )) + ((e * c) ^2 )) + ((b * f) ^2 )) + ((e * d) ^2 )
A1: 0 <= ((a * d) - (c * b)) ^2 by XREAL_1:65;
A2: 0 <= ((a * f) - (e * c)) ^2 by XREAL_1:65;
0 <= ((b * f) - (e * d)) ^2 by XREAL_1:65;
then 0 + 0 <= (((a * f) - (e * c)) ^2 ) + (((b * f) - (e * d)) ^2 ) by A2, XREAL_1:9;
then 0 + 0 <= (((a * d) - (c * b)) ^2 ) + ((((a * f) - (e * c)) ^2 ) + (((b * f) - (e * d)) ^2 )) by A1, XREAL_1:9;
then 0 <= (((((a * d) ^2 ) + ((c * b) ^2 )) + (((a * f) - (e * c)) ^2 )) + (((b * f) - (e * d)) ^2 )) - ((2 * (a * d)) * (c * b)) ;
then 0 + ((2 * (a * d)) * (c * b)) <= ((((a * d) ^2 ) + ((c * b) ^2 )) + (((a * f) - (e * c)) ^2 )) + (((b * f) - (e * d)) ^2 ) by XREAL_1:21;
then (2 * (a * d)) * (c * b) <= ((((((a * d) ^2 ) + ((c * b) ^2 )) + ((a * f) ^2 )) + ((e * c) ^2 )) + (((b * f) - (e * d)) ^2 )) - ((2 * (a * f)) * (e * c)) ;
then ((2 * (a * d)) * (c * b)) + ((2 * (a * f)) * (e * c)) <= (((((((a * d) ^2 ) + ((c * b) ^2 )) + ((a * f) ^2 )) + ((e * c) ^2 )) + ((b * f) ^2 )) + ((e * d) ^2 )) - ((2 * (b * f)) * (e * d)) by XREAL_1:21;
hence (((2 * (a * d)) * (c * b)) + ((2 * (a * f)) * (e * c))) + ((2 * (b * f)) * (e * d)) <= ((((((a * d) ^2 ) + ((c * b) ^2 )) + ((a * f) ^2 )) + ((e * c) ^2 )) + ((b * f) ^2 )) + ((e * d) ^2 ) by XREAL_1:21; :: thesis: verum