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