theorem Th8: :: DIOPHAN1:7
for n being Nat
for r being Real st r is irrational holds
(c_d r) . n >= 1