:: deftheorem defines Necklace NECKLACE:def 9 :
for n being Nat holds Necklace n = SymRelStr (n -SuccRelStr);