theorem Th48: :: SERIES_5:48

for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((n + 1) ^2) ) holds
for n being Nat holds (Partial_Sums s) . n <= 2 - (1 / (n + 1))