theorem Th18: :: SERIES_3:18

for x, y being Real st x + y = 1 holds
x * y <= 1 / 4