let n be non zero Nat; :: thesis: ln . (n + 1) > 0
0 + 1 < n + 1 by XREAL_1:8;
hence ln . (n + 1) > 0 by LogZero, LogMono; :: thesis: verum