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;