:: deftheorem Def2 defines ~= OSALG_1:def 2 :
for S being non empty non void OverloadedMSSign
for x, y being OperSymbol of S holds
( x ~= y iff [x,y] in the Overloading of S );