:: deftheorem defines OperNames OSALG_1:def 23 :
for S being OrderSortedSign holds OperNames S = Class the Overloading of S;