theorem Th50: :: SERIES_5:50
for s being Real_Sequence st ( for n being Nat holds s . n < 1 ) holds
for n being Nat holds (Partial_Sums s) . n < n + 1