:: deftheorem Def6 defines -SuccRelStr NECKLACE:def 6 :
for n being Nat
for b₂ being strict RelStr holds
( b₂ = n -SuccRelStr iff ( the carrier of b₂ = n & the InternalRel of b₂ = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) );