theorem :: SERIES_3:19

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