let x, y be Real; :: thesis: ( x + y = 1 implies (x ^2) + (y ^2) >= 1 / 2 )
(x - y) ^2 >= 0 by XREAL_1:63;
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:7;
assume x + y = 1 ; :: thesis: (x ^2) + (y ^2) >= 1 / 2
then 1 ^2 = ((x ^2) + ((2 * x) * y)) + (y ^2) by SQUARE_1:4;
then (2 * ((x ^2) + (y ^2))) / 2 >= 1 / 2 by A1, XREAL_1:72;
hence (x ^2) + (y ^2) >= 1 / 2 ; :: thesis: verum