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