theorem :: REAL_3:46

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