set R = the InternalRel of A;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then A1: field the InternalRel of A = the carrier of A by ORDERS_1:13;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
hence the InternalRel of A is reflexive by A1; :: thesis: verum