let a, b, c be positive Real; :: thesis: (a + b) + c >= 3 * (3 -root ((a * b) * c))
A1: 3 -Root c > 0 by PREPOWER:def 2;
( 3 -Root a > 0 & 3 -Root b > 0 ) by PREPOWER:def 2;
then (((3 -Root a) |^ 3) + ((3 -Root b) |^ 3)) + ((3 -Root c) |^ 3) >= ((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c) by A1, Th12;
then (a + ((3 -Root b) |^ 3)) + ((3 -Root c) |^ 3) >= ((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c) by PREPOWER:19;
then (a + b) + ((3 -Root c) |^ 3) >= ((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c) by PREPOWER:19;
then (a + b) + c >= (3 * ((3 -Root a) * (3 -Root b))) * (3 -Root c) by PREPOWER:19;
then (a + b) + c >= (3 * (3 -Root (a * b))) * (3 -Root c) by PREPOWER:22;
then (a + b) + c >= 3 * ((3 -Root (a * b)) * (3 -Root c)) ;
then (a + b) + c >= 3 * (3 -Root ((a * b) * c)) by PREPOWER:22;
hence (a + b) + c >= 3 * (3 -root ((a * b) * c)) by POWER:def 1; :: thesis: verum