theorem :: SERIES_3:48

for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds
(Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4))