:: deftheorem defines <= OSALG_1:def 20 :
for S being OrderSortedSign
for o1, o2 being OperSymbol of S holds
( o1 <= o2 iff ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) );