theorem Th21: :: DIOPHAN1:20

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