b >= 1 + 1 by NAT_2:29;
then b > 1 by NAT_1:13;
hence powerfact b is summable by Th26; :: thesis: verum