theorem Th9: :: SERIES_3:9

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