theorem Th16: :: DIOPHAN1:15

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