theorem LmNT: :: NEWTON03:98

for n being Nat
for a being non trivial Nat holds ((a + 1) |^ n) + ((a + 1) |^ n) < (a + 1) |^ (n + 1)