let F be Function of NAT,ExtREAL; :: thesis: ( F is nonnegative & ex n being Element of NAT st F . n = +infty implies not F is summable )
assume A1: F is nonnegative ; :: thesis: ( for n being Element of NAT holds not F . n = +infty or not F is summable )
assume ex n being Element of NAT st F . n = +infty ; :: thesis: not F is summable
then not SUM F in REAL by A1, Th64;
hence not F is summable by Def24; :: thesis: verum