theorem Th22: :: DIOPHAN2:18
for a, b being Real
for n being Integer st |.(n - a).| * |.((n + 1) - a).| <= 1 / 4 & |.(n - b).| * |.((n + 1) - b).| <= 1 / 4 & not |.(n - a).| * |.(n - b).| <= 1 / 4 holds
|.((n + 1) - a).| * |.((n + 1) - b).| <= 1 / 4