theorem :: SERIES_5:55

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