theorem Th4: :: SERIES_3:4

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