theorem Th16: :: METRIC_3:16

for a, b, c, d, e, f being Real holds (((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)