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