theorem Diesel2: :: MOEBIUS3:15

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