for b being Nat st b > 1 holds
( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) )