let a, b be Real; :: thesis: ( a is not Integer & [\a/] > 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/] > b ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )
assume A3: for u being Integer st |.(a - u).| < 1 holds
|.(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 ( |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 ) by A3, A4;
hence contradiction by A1, A2, Th32; :: thesis: verum