theorem Th30: :: OSALG_1:30

for S being OrderSortedSign
for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) )