theorem Th8: :: DIOPHAN1:8

for n being Nat
for r being Real st r is irrational holds
(c_d r) . n >= 1