theorem Th26: :: DIOPHAN2:22

for a, b being Real
for n being Integer st (n - a) * ((n + 1) - b) > 0 & (b - n) * ((n + 1) - a) > 0 holds
( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )