theorem Th28: :: DIOPHAN2:24

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