:: deftheorem Def7 defines SymRelStr NECKLACE:def 7 :
for R being RelStr
for b₂ being strict RelStr holds
( b₂ = SymRelStr R iff ( the carrier of b₂ = the carrier of R & the InternalRel of b₂ = the InternalRel of R \/ ( the InternalRel of R ~) ) );