theorem Th10: :: DIOPHAN1:10
for n being Nat
for r being Real st r is irrational holds
(c_d r) . n >= n