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