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