:: deftheorem Def3 defines symmetric NECKLACE:def 3 :
for R being RelStr holds
( R is symmetric iff the InternalRel of R is_symmetric_in the carrier of R );