let a, b be Real; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

per cases ( a in INT or not a in INT ) ;

suppose A: a in INT ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

|.(a - a).| * |.(b - a).| = 0 ;
hence ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) ) by A; :: thesis: verum

end;

suppose not a in INT ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

then A5: not a is integer ;

per cases ( ( [\a/] <= b & b <= [\a/] + 1 ) or b < [\a/] or [\a/] + 1 < b ) ;

suppose ( [\a/] <= b & b <= [\a/] + 1 ) ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

then ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 ) by Th28, A5;
hence ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) ) ; :: thesis: verum

end;

suppose b < [\a/] ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

then ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) by Th33, A5;
hence ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) ) ; :: thesis: verum

end;

suppose [\a/] + 1 < b ; :: thesis: ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

then ex u being Integer st
( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) by Th39, A5;
hence ex u being Integer st
( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) ) ; :: thesis: verum

end;

end;

end;

end;