for a, b, c, k, m being Nat st c |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 & k > 0 holds
c |^ (k + m) > (a |^ (k + m)) + (b |^ (k + m))