theorem :: MOEBIUS3:13

for x being Real st x > 0 holds
exp_R . x > x + 1