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