:: deftheorem defines Name OSALG_1:def 24 :
for S being OrderSortedSign
for op1 being OperSymbol of S holds Name op1 = Class ( the Overloading of S,op1);