let a, b, c, m be Nat; :: thesis: ( (a |^ m) + (b |^ m) <= c |^ m implies ex x being Nat st (a |^ m) + (b |^ m) <= (a + x) |^ m )
assume A1: (a |^ m) + (b |^ m) <= c |^ m ; :: thesis: ex x being Nat st (a |^ m) + (b |^ m) <= (a + x) |^ m
then ex x being Nat st c = a + x by Th6, NAT_1:10;
hence ex x being Nat st (a |^ m) + (b |^ m) <= (a + x) |^ m by A1; :: thesis: verum