theorem Th24: :: DIOPHAN1:23

for n being Nat
for r being Real st r is irrational holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)