let r be Real; :: thesis: ex n being Nat st
( - n < r & r < n )

per cases ( 0 <= r or r < 0 ) ;

suppose A1: 0 <= r ; :: thesis: ex n being Nat st
( - n < r & r < n )

consider n being Nat such that
A2: r < n by SEQ_4:3;
- n < 0 by A2, A1;
hence ex n being Nat st
( - n < r & r < n ) by A1, A2; :: thesis: verum

end;

suppose A3: r < 0 ; :: thesis: ex n being Nat st
( - n < r & r < n )

consider n being Nat such that
A4: - r < n by SEQ_4:3;
0 - r < n by A4;
then ( - n = 0 - n & 0 - n < r & r < 0 & 0 <= n ) by A3, XREAL_1:11;
hence ex n being Nat st
( - n < r & r < n ) ; :: thesis: verum

end;

end;