theorem Th23: :: NECKLACE:24

for n, i, j being Nat holds
( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )