theorem :: PRE_FF:17

for n being Nat holds n < (2 * n) + 1