let x be OperSymbol of S; :: thesis: [x,x] in the Overloading of S
field the Overloading of S = the carrier' of S by ORDERS_1:12;
then the Overloading of S is_reflexive_in the carrier' of S by RELAT_2:def 9;
hence [x,x] in the Overloading of S by RELAT_2:def 1; :: thesis: verum