let O be non empty RelStr ; :: thesis: ( O is antisymmetric implies O is SubAntisymmetric )
set RO = the InternalRel of O;
assume O is antisymmetric ; :: thesis: O is SubAntisymmetric
then the InternalRel of O is_antisymmetric_in the carrier of O by ORDERS_2:def 6;
then the InternalRel of O is antisymmetric by Th11;
hence O is SubAntisymmetric by Def15; :: thesis: verum