let f, g be summable Real_Sequence; :: thesis: ( ( for n being Nat holds f . n <= g . n ) implies Sum f <= Sum g )
A1: ( Sum f = lim (Partial_Sums f) & Sum g = lim (Partial_Sums g) ) by SERIES_1:def 3;
assume for n being Nat holds f . n <= g . n ; :: thesis: Sum f <= Sum g
then A2: for n being Nat holds (Partial_Sums f) . n <= (Partial_Sums g) . n by SERIES_1:14;
( Partial_Sums f is convergent & Partial_Sums g is convergent ) by SERIES_1:def 2;
hence Sum f <= Sum g by A1, A2, SEQ_2:18; :: thesis: verum