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 Def4, ORDERS_1:12;
hence the InternalRel of A is antisymmetric ; :: thesis: verum