for m being Nat holds (2 |^ (3 + m)) + (2 |^ (3 + m)) < 3 |^ (3 + m)