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