let a, b be Real; :: thesis: ( a is not Integer & [\a/] <= b & b <= [\a/] + 1 implies ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 ) )
assume that
A1: a is not Integer and
A2: ( [\a/] <= b & b <= [\a/] + 1 ) ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 )
set n = [\a/];
A3: [\a/] < a by A1, INT_1:26;
a - 1 < [\a/] by INT_1:def 6;
then a < [\a/] + 1 by XREAL_1:19;
then A6: |.([\a/] - a).| * |.(([\a/] + 1) - a).| <= 1 / 4 by Th17, A3;
|.([\a/] - b).| * |.(([\a/] + 1) - b).| <= 1 / 4 by Th17, A2;

per cases then ( |.([\a/] - a).| * |.([\a/] - b).| <= 1 / 4 or |.(([\a/] + 1) - a).| * |.(([\a/] + 1) - b).| <= 1 / 4 ) by Th22, A6;

suppose A8: |.([\a/] - a).| * |.([\a/] - b).| <= 1 / 4 ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 )

set u = [\a/];
A10: |.(a - [\a/]).| < 1 by A1, Th21;
|.([\a/] - a).| * |.([\a/] - b).| = |.(a - [\a/]).| * |.([\a/] - b).| by COMPLEX1:60
.= |.(a - [\a/]).| * |.(b - [\a/]).| by COMPLEX1:60 ;
hence ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 ) by A10, A8; :: thesis: verum

end;

suppose A12: |.(([\a/] + 1) - a).| * |.(([\a/] + 1) - b).| <= 1 / 4 ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 )

set u = [\a/] + 1;
A14: |.(a - ([\a/] + 1)).| < 1 by A1, Th21;
|.(([\a/] + 1) - a).| * |.(([\a/] + 1) - b).| = |.(a - ([\a/] + 1)).| * |.(([\a/] + 1) - b).| by COMPLEX1:60
.= |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| by COMPLEX1:60 ;
hence ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 ) by A14, A12; :: thesis: verum

end;

end;