theorem Th9: :: HOLDER_1:9

for a, b, c being Real_Sequence st ( for n being Nat holds a . n <= (b . n) + (c . n) ) & b is convergent & c is convergent & a is non-decreasing holds
( a is convergent & lim a <= (lim b) + (lim c) )