theorem :: SERIES_5:45
for n being Nat st n >= 1 holds
(1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1)