:: deftheorem Def7 defines monotone OSALG_1:def 7 :
for S being OrderSortedSign
for o being OperSymbol of S holds
( o is monotone iff for o2 being OperSymbol of S st o ~= o2 & the_arity_of o <= the_arity_of o2 holds
the_result_sort_of o <= the_result_sort_of o2 );