let a, b, c, d, e, f be real number ; :: 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 Th13;
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:8;
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:8;
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:8;
hence (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2 ) + (b ^2 )) + (e ^2 )) * (((c ^2 ) + (d ^2 )) + (f ^2 )) ; :: thesis: verum