let x be Real; :: thesis: ex y being non zero Nat st x < ln . (ln . (y + 1))
set N = [/(exp_R . (exp_R . x))\];
A1: exp_R . (exp_R . x) > 0 by SIN_COS:54;
then [/(exp_R . (exp_R . x))\] > 0 by INT_1:def 7;
then [/(exp_R . (exp_R . x))\] in NAT by INT_1:3;
then reconsider N = [/(exp_R . (exp_R . x))\] as non zero Nat by SIN_COS:54, INT_1:def 7;
take N ; :: thesis: x < ln . (ln . (N + 1))
A3: exp_R . x > 0 by SIN_COS:54;
ln . (exp_R . (exp_R . x)) < ln . (N + 1) by A1, LogMono, INT_1:32;
then exp_R . x < ln . (N + 1) by LogExp;
then ln . (exp_R . x) < ln . (ln . (N + 1)) by A3, LogMono;
hence x < ln . (ln . (N + 1)) by LogExp; :: thesis: verum