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

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

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

thus ex n being Element of NAT st - n <= r by A2, A3; :: 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;