let a, b, m be Nat; :: thesis: (a |^ (m + 1)) + (b |^ (m + 1)) >= (((a |^ m) + (b |^ m)) * (a + b)) / 2
A1: (a |^ (m + 1)) + (b |^ (m + 1)) = ((((a |^ m) + (b |^ m)) * (a + b)) + ((a - b) * ((a |^ m) - (b |^ m)))) / 2 by Th9
.= ((((a |^ m) + (b |^ m)) * (a + b)) / 2) + (((a - b) * ((a |^ m) - (b |^ m))) / 2) ;
(((a |^ m) + (b |^ m)) * (a + b)) + ((a - b) * ((a |^ m) - (b |^ m))) >= ((a |^ m) + (b |^ m)) * (a + b) by Th10, XREAL_1:31;
then ((((a |^ m) + (b |^ m)) * (a + b)) + ((a - b) * ((a |^ m) - (b |^ m)))) / 2 >= (((a |^ m) + (b |^ m)) * (a + b)) / 2 by XREAL_1:72;
hence (a |^ (m + 1)) + (b |^ (m + 1)) >= (((a |^ m) + (b |^ m)) * (a + b)) / 2 by A1; :: thesis: verum