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