theorem :: NUMBER09:63
for n being Nat holds ((((n + 1) |^ 3) + ((n + 2) |^ 3)) + ((n + 3) |^ 3)) + ((n + 4) |^ 3) <> (n + 5) |^ 3