theorem Th58: :: REAL_3:58

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