theorem :: REAL_3:54

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