:: deftheorem defines asymmetric NECKLACE:def 4 :
for R being RelStr holds
( R is asymmetric iff the InternalRel of R is asymmetric );