theorem Th26: :: LIOUVIL1:27
for b being Nat st b > 1 holds
( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) )