theorem Th41: :: DIOPHAN2:29

for a, b being Real ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )