let x be Real; :: thesis: ( x > 0 implies ln . (x + 1) < x )
assume x > 0 ; :: thesis: ln . (x + 1) < x
then x + 1 > 1 by XREAL_1:29;
then ln . (x + 1) < (x + 1) - 1 by ENTROPY1:2;
hence ln . (x + 1) < x ; :: thesis: verum