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