theorem Th38: :: SERIES_3:38

for n being Nat
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) holds
(n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n