for eps being ExtReal st 0. < eps holds
ex F being sequence of ExtREAL st
( ( for n being Nat holds 0. < F . n ) & SUM F < eps )