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