theorem Th6: :: CARDFIN2:6

for n being positive Nat
for c being Real st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2