theorem Th26: :: NECKLACE:27

for n being Nat st n > 0 holds
card the InternalRel of (Necklace n) = 2 * (n - 1)