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