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