theorem Th31: :: OSALG_1:31

for S being OrderSortedSign
for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff Name op1 = Name op2 )