set R = the InternalRel of A;
the InternalRel of A is_reflexive_in the carrier of A by Def4;
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 Def4;
hence the InternalRel of A is reflexive by A1, RELAT_2:def 9; :: thesis: verum