:: deftheorem Def8 defines ComplRelStr NECKLACE:def 8 :
for R being RelStr
for b₂ being strict RelStr holds
( b₂ = ComplRelStr R iff ( the carrier of b₂ = the carrier of R & the InternalRel of b₂ = ( the InternalRel of R `) \ (id the carrier of R) ) );