theorem Th2: :: INT_1:2

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