let a, b be Real; :: thesis: ( a is not Integer & [\a/] + 1 < b implies ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )
assume that
A1: a is not Integer and
A2: [\a/] + 1 < b ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )
assume A3: for u being Integer holds
( not |.(a - u).| < 1 or not |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) ; :: thesis: contradiction
set u = [\a/];
set v = [\a/] + 1;
A4: |.(a - [\a/]).| < 1 by A1, Th21;
|.(a - ([\a/] + 1)).| < 1 by A1, Th21;
then b1: |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 by A3;
|.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 by A3, A4;
hence contradiction by A1, A2, Th37, b1; :: thesis: verum