theorem :: REAL_3:55

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