theorem Th3: :: NIVEN:3
for i being Integer holds
( not |.i.| <= 2 or i = - 2 or i = - 1 or i = 0 or i = 1 or i = 2 )