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