theorem :: MOEBIUS3:22

for n being non zero Nat holds ln . (n + 1) < Harmonic n