for r being Real st r is Integer holds
ex k being Nat st
( r = k or r = - k )