let q be Element of REAL ; :: thesis: ex m being Element of INT st |.(q - m).| <= 1 / 2

per cases ( |.(q - [\q/]).| <= 1 / 2 or not |.(q - [\q/]).| <= 1 / 2 ) ;

suppose A1: |.(q - [\q/]).| <= 1 / 2 ; :: thesis: ex m being Element of INT st |.(q - m).| <= 1 / 2

reconsider m = [\q/] as Element of INT by INT_1:def 2;
take m ; :: thesis: |.(q - m).| <= 1 / 2
thus |.(q - m).| <= 1 / 2 by A1; :: thesis: verum

end;

suppose A2: not |.(q - [\q/]).| <= 1 / 2 ; :: thesis: ex m being Element of INT st |.(q - m).| <= 1 / 2

0 <= q - [\q/] by INT_1:def 6, XREAL_1:48;
then 1 / 2 < q - [\q/] by A2, ABSVALUE:def 1;
then (1 / 2) - 1 <= (q - [\q/]) - 1 by XREAL_1:9;
then A3: - (1 / 2) <= q - ([\q/] + 1) ;
q - ([\q/] + 1) <= ([\q/] + 1) - ([\q/] + 1) by INT_1:29, XREAL_1:9;
then A4: q - ([\q/] + 1) <= 0 ;
reconsider m = [\q/] + 1 as Element of INT by INT_1:def 2;
take m ; :: thesis: |.(q - m).| <= 1 / 2
thus |.(q - m).| <= 1 / 2 by A3, A4, ABSVALUE:5; :: thesis: verum

end;

end;