theorem :: REAL_3:53

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