for x, y, z being Real holds ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z)