let a, b, c be positive Real; :: thesis: ((a + b) + c) / 3 >= 3 -root ((a * b) * c)
((a + b) + c) / 3 >= (3 * (3 -root ((a * b) * c))) / 3 by Th15, XREAL_1:72;
hence ((a + b) + c) / 3 >= 3 -root ((a * b) * c) ; :: thesis: verum