let x, y be OperSymbol of S; :: thesis: ( [x,y] in the Overloading of S implies [y,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_symmetric_in the carrier' of S by RELAT_2:def 11;
hence ( [x,y] in the Overloading of S implies [y,x] in the Overloading of S ) by RELAT_2:def 3; :: thesis: verum