let r be Real; :: thesis:
[\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 < 0 or [\r/] >= 0 ) ;

suppose [\r/] < 0 ; :: thesis:

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

end;

suppose A2: [\r/] >= 0 ; :: thesis:

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

end;

end;