theorem Th3: :: OSALG_1:3

for S being non empty non void OverloadedMSSign holds
( S is op-discrete iff for x, y being OperSymbol of S st x ~= y holds
x = y )