theorem Th10: :: DIOPHAN1:9

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