let S be OrderSortedSign; :: thesis: for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) )
let op1, op2 be OperSymbol of S; :: thesis: ( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) )
( op1 ~= op2 iff [op2,op1] in the Overloading of S ) by Def2;
hence ( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) ) by EQREL_1:19; :: thesis: verum