let S be non empty non void OverloadedMSSign ; :: thesis: for o, o1, o2 being OperSymbol of S st o ~= o1 & o1 ~= o2 holds
o ~= o2
let o, o1, o2 be OperSymbol of S; :: thesis: ( o ~= o1 & o1 ~= o2 implies o ~= o2 )
field the Overloading of S = the carrier' of S by ORDERS_1:12;
then A1: the Overloading of S is_transitive_in the carrier' of S by RELAT_2:def 16;
assume ( o ~= o1 & o1 ~= o2 ) ; :: thesis: o ~= o2
then ( [o,o1] in the Overloading of S & [o1,o2] in the Overloading of S ) ;
then [o,o2] in the Overloading of S by A1, RELAT_2:def 8;
hence o ~= o2 ; :: thesis: verum