let x, y be real number ; :: thesis: ( x + y = 1 implies (x ^2 ) + (y ^2 ) >= 1 / 2 )
(x - y) ^2 >= 0 by XREAL_1:65;
then A1: (((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + (((x ^2 ) + ((2 * x) * y)) + (y ^2 )) >= 0 + (((x ^2 ) + ((2 * x) * y)) + (y ^2 )) by XREAL_1:9;
assume x + y = 1 ; :: thesis: (x ^2 ) + (y ^2 ) >= 1 / 2
then 1 ^2 = ((x ^2 ) + ((2 * x) * y)) + (y ^2 ) by SQUARE_1:63;
then (2 * ((x ^2 ) + (y ^2 ))) / 2 >= 1 / 2 by A1, XREAL_1:74;
hence (x ^2 ) + (y ^2 ) >= 1 / 2 ; :: thesis: verum