theorem Th8: :: SERIES_3:8

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