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

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