for n being Nat st n <> 0 holds
(n + 1) / n > 1