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