for n being Nat
for r being Real st r is irrational holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| > 0