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 Segm n by Th19;
hence i < n by NAT_1:44; :: thesis: verum