let a, b be Real; :: thesis: 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 )
let n be Integer; :: thesis: ( 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 )
assume A1: ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 ; :: thesis: ( |.(a - n).| * |.(b - n).| <= |.(a - b).| / 2 or |.((a - n) - 1).| * |.((b - n) - 1).| <= |.(a - b).| / 2 )
set r1 = |.(a - n).|;
set r2 = |.(b - n).|;
set s1 = |.((a - n) - 1).|;
set s2 = |.((b - n) - 1).|;
set t = a - b;
set r0 = |.(a - b).| / 2;
set r3 = |.(a - n).| * |.(b - n).|;
set r4 = |.((a - n) - 1).| * |.((b - n) - 1).|;
A3: sqrt ((|.(a - b).| ^2) / 4) = sqrt ((|.(a - b).| / 2) * (|.(a - b).| / 2))
.= (sqrt (|.(a - b).| / 2)) ^2 by SQUARE_1:29
.= |.(a - b).| / 2 by SQUARE_1:def 2 ;
(|.(a - n).| * |.(b - n).|) * (|.((a - n) - 1).| * |.((b - n) - 1).|) <= (|.(a - b).| ^2) / 4 by A1;
hence ( |.(a - n).| * |.(b - n).| <= |.(a - b).| / 2 or |.((a - n) - 1).| * |.((b - n) - 1).| <= |.(a - b).| / 2 ) by A3, Th18; :: thesis: verum