theorem :: SUPINF_2:46

for F being sequence of ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds
not F is summable by Th44;