theorem Th1: :: INT_1:1

for r being Real
for k being natural Number st ( r = k or r = - k ) holds
r is Integer