theorem Th20: :: NECKLACE:21
for n, i being Nat st i + 1 < n holds
[i,(i + 1)] in the InternalRel of (Necklace n)