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

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

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

hence ex n being Nat st - n <= r by A1; :: thesis: verum

end;

suppose A2: [\r/] >= 0 ; :: thesis: ex n being Nat st - n <= r

take 0 ; :: thesis: - 0 <= r
thus - 0 <= r by A2, INT_1:def 6; :: thesis: verum

end;

end;