theorem :: REAL_3:75

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat st n >= 1 holds
((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1))