theorem Th7: :: SERIES_3:7

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