theorem Th2: :: OSALG_1:2

for S being non empty non void OverloadedMSSign
for o, o1, o2 being OperSymbol of S st o ~= o1 & o1 ~= o2 holds
o ~= o2