theorem :: SERIES_3:5

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