theorem Th12: :: DIOPHAN1:11

for n being Nat
for r being Real st r is irrational holds
( (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) > 0 & (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) - ((c_d r) . n) > 0 )