:: deftheorem defines summable SUPINF_2:def 13 :
for F being sequence of ExtREAL holds
( F is summable iff SUM F in REAL );