theorem Th1: :: BOR_CANT:1

for k being Element of NAT
for x being Element of REAL st k is odd & x > 0 & x <= 1 holds
(((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0