theorem Th16: :: DIOPHAN1:16

for n being Nat
for r being Real st r is irrational & n is natural even number & n > 0 holds
r > ((c_n r) . n) / ((c_d r) . n)