let n, i be Nat; :: thesis: ( i in the carrier of (Necklace n) implies i < n )
assume i in the carrier of (Necklace n) ; :: thesis: i < n
then i in n by Th21;
hence i < n by NAT_1:44; :: thesis: verum