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