:: deftheorem Def14 defines LBound OSALG_1:def 14 :
for SR being monotone regular OrderSortedSign
for o being OperSymbol of SR
for w1 being Element of the carrier of SR * st w1 <= the_arity_of o holds
for b₄ being OperSymbol of SR holds
( b₄ = LBound (o,w1) iff b₄ has_least_args_for o,w1 );