theorem Th19: :: NAT_6:19

for n being Nat holds
( - 1,1 are_congruent_mod n iff ( n = 2 or n = 1 ) )