theorem Th25: :: DIOPHAN2:21

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