theorem Th6: :: SERIES_3:6

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