theorem Th20: :: NAT_6:20

for i being Integer holds
( - 1,1 are_congruent_mod i iff ( i = 2 or i = 1 or i = - 2 or i = - 1 ) )