let n be Nat; :: thesis: the carrier of (Necklace n) = n
the carrier of (Necklace n) = the carrier of (n -SuccRelStr) by Def8
.= n by Def7 ;
hence the carrier of (Necklace n) = n ; :: thesis: verum