let a, b, c, d, e, f be Real; :: thesis: (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2))
(((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 Th16;
then ((e * f) ^2) + ((((2 * (a * b)) * (c * d)) + ((2 * (a * c)) * (e * f))) + ((2 * (b * d)) * (e * f))) <= (((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) + ((e * f) ^2) by XREAL_1:6;
then ((b * d) ^2) + (((e * f) ^2) + ((((2 * (a * b)) * (c * d)) + ((2 * (a * c)) * (e * f))) + ((2 * (b * d)) * (e * f)))) <= ((((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) + ((e * f) ^2)) + ((b * d) ^2) by XREAL_1:6;
then ((a * c) ^2) + (((b * d) ^2) + (((e * f) ^2) + ((((2 * (a * b)) * (c * d)) + ((2 * (a * c)) * (e * f))) + ((2 * (b * d)) * (e * f))))) <= (((((((((a * d) ^2) + ((c * b) ^2)) + ((a * f) ^2)) + ((e * c) ^2)) + ((b * f) ^2)) + ((e * d) ^2)) + ((e * f) ^2)) + ((b * d) ^2)) + ((a * c) ^2) by XREAL_1:6;
hence (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2)) ; :: thesis: verum