theorem Th24: :: NECKLACE:25

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