let O be non empty RelStr ; :: thesis: ( O is asymmetric implies O is irreflexive )
set R = the InternalRel of O;
assume O is asymmetric ; :: thesis: O is irreflexive
then the InternalRel of O is asymmetric by NECKLACE:def 4;
then the InternalRel of O is irreflexive by RELAT_2:9;
hence O is irreflexive by Def11; :: thesis: verum