let O be non empty RelStr ; :: thesis: ( O is irreflexive & O is asymmetric implies O is Asymmetric )
set IntRel = the InternalRel of O;
set CO = the carrier of O;
assume ( O is irreflexive & O is asymmetric ) ; :: thesis: O is Asymmetric
then the InternalRel of O is asymmetric by NECKLACE:def 5;
then the InternalRel of O is_asymmetric_in the carrier of O by Th14;
hence O is Asymmetric by Def18; :: thesis: verum