let x, y be Real; :: thesis: ( x + y = 1 implies (x |^ 3) + (y |^ 3) >= 1 / 4 )
assume A1: x + y = 1 ; :: thesis: (x |^ 3) + (y |^ 3) >= 1 / 4
then (x * y) * (- 3) >= (1 / 4) * (- 3) by Th18, XREAL_1:65;
then A2: 1 + ((x * y) * (- 3)) >= ((1 / 4) * (- 3)) + 1 by XREAL_1:7;
(x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2)) by Lm6;
then (x |^ 3) + (y |^ 3) = (((x ^2) + ((2 * x) * y)) + (y ^2)) - ((3 * x) * y) by A1
.= (1 ^2) - (3 * (x * y)) by A1, SQUARE_1:4 ;
hence (x |^ 3) + (y |^ 3) >= 1 / 4 by A2; :: thesis: verum