theorem Th23: :: DIOPHAN1:22

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