:: deftheorem defines has_least_args_for OSALG_1:def 9 :
for S being OrderSortedSign
for o, o1 being OperSymbol of S
for w1 being Element of the carrier of S * holds
( o1 has_least_args_for o,w1 iff ( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_arity_of o1 <= the_arity_of o2 ) ) );