let a, b, x, m be Nat; :: thesis: ( (a + x) |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 implies x > 0 )
assume ( (a + x) |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 ) ; :: thesis: x > 0
then x <> 0 by Lm5c;
hence x > 0 ; :: thesis: verum