theorem :: MEASUR12:47

for f, g being sequence of ExtREAL st f is nonnegative & ex N being Nat st
( (Ser f) . N <= (Ser g) . N & ( for n being Nat st n > N holds
f . n <= g . n ) ) holds
SUM f <= SUM g