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