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