theorem :: NECKLACE:30
for n being Nat holds
( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )