:: deftheorem Def12 defines regular OSALG_1:def 12 :
for S being OrderSortedSign
for o being OperSymbol of S holds
( o is regular iff ( o is monotone & ( for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of S st o1 has_least_args_for o,w1 ) ) );