let a, b, c, d, e, f be real number ; (((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 )
( 0 <= ((a * f) - (e * c)) ^2 & 0 <= ((b * f) - (e * d)) ^2 )
by XREAL_1:65;
then
( 0 <= ((a * d) - (c * b)) ^2 & 0 + 0 <= (((a * f) - (e * c)) ^2 ) + (((b * f) - (e * d)) ^2 ) )
by XREAL_1:9, XREAL_1:65;
then
0 + 0 <= (((a * d) - (c * b)) ^2 ) + ((((a * f) - (e * c)) ^2 ) + (((b * f) - (e * d)) ^2 ))
by 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; verum