theorem :: REAL_3:59

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