theorem :: SERIES_3:11
for x, y, z being Real holds ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z))