theorem :: MOEBIUS3:20

for x being Real ex y being non zero Nat st x < ln . (ln . (y + 1))