theorem Th7: :: DIOPHAN1:6

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