let a, b be Real; :: thesis: for n being Integer st n + 1 < b & n < a & a < n + 1 holds
((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4
let n be Integer; :: thesis: ( n + 1 < b & n < a & a < n + 1 implies ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )
assume A2: ( n + 1 < b & n < a & a < n + 1 ) ; :: thesis: ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4
then A3: (n + 1) - b < 0 by XREAL_1:49;
A4: n - a < 0 by A2, XREAL_1:49;
A5: (1 + n) - n < b - n by A2, XREAL_1:14;
A6: (n + 1) - a > 0 by A2, XREAL_1:50;
A7: (n - a) * ((n + 1) - b) > 0 by A3, A4;
(b - n) * ((n + 1) - a) > 0 by A5, A6;
hence ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 by A7, Th26; :: thesis: verum