theorem :: SERIES_5:57

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