theorem Th18: :: NECKLACE:19

for n being Nat
for x being set holds
( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )