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