for n, i being Nat st i in the carrier of (Necklace n) holds
i < n