theorem Th39: :: DIOPHAN2:28

for a, b being Real st a is not Integer & [\a/] + 1 < b holds
ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )