theorem Th23: :: DIOPHAN2:19

for a, b being Real
for n being Integer holds
( not ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 or |.(a - n).| * |.(b - n).| <= |.(a - b).| / 2 or |.((a - n) - 1).| * |.((b - n) - 1).| <= |.(a - b).| / 2 )