theorem Th21: :: NECKLACE:22

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