let a be Integer; :: thesis: for b being Real st |.(a - b).| < 1 / 2 holds
a = round b
let b be Real; :: thesis: ( |.(a - b).| < 1 / 2 implies a = round b )
assume A1: |.(a - b).| < 1 / 2 ; :: thesis: a = round b
then a - b < 1 / 2 by SEQ_2:1;
then A2: (a - b) + b < (1 / 2) + b by XREAL_1:8;
- (1 / 2) < a - b by A1, SEQ_2:1;
then - (a - b) < - (- (1 / 2)) by XREAL_1:24;
then (b - a) + a < (1 / 2) + a by XREAL_1:8;
then b - (1 / 2) < (a + (1 / 2)) - (1 / 2) by XREAL_1:14;
then (b + (1 / 2)) - 1 < a ;
hence a = round b by A2, INT_1:def 6; :: thesis: verum