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