let r be Real; :: thesis: ex n being Element of NAT st - n <= r
[\r/] is Element of INT by INT_1:def 2;
then A2: ( [\r/] <= r & ex k being Element of NAT st
( [\r/] = k or [\r/] = - k ) ) by INT_1:def 1, INT_1:def 4;

per cases ( [\r/] < 0 or [\r/] >= 0 ) ;

suppose [\r/] < 0 ; :: thesis: ex n being Element of NAT st - n <= r

hence ex n being Element of NAT st - n <= r by A2; :: thesis: verum

end;

suppose A4: [\r/] >= 0 ; :: thesis: ex n being Element of NAT st - n <= r

take 0 ; :: thesis: - 0 <= r
thus - 0 <= r by A4, INT_1:def 4; :: thesis: verum

end;

end;