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

( |.(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