theorem Th39: :: IRRAT_1:39

for n being Nat
for x being Real st n > 0 & x = 1 / (n + 1) holds
(n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)