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