:: deftheorem defines irreflexive NECKLACE:def 5 :
for R being RelStr holds
( R is irreflexive iff for x being set st x in the carrier of R holds
not [x,x] in the InternalRel of R );