theorem Th17: :: METRIC_3:17

for a, b, c, d, e, f being Real holds (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2))