set R = the InternalRel of A;
( field the InternalRel of A = the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A ) by Def6, ORDERS_1:12;
hence the InternalRel of A is antisymmetric by RELAT_2:def 12; :: thesis: verum