:: deftheorem defines LBound OSALG_1:def 25 :
for SR being monotone regular OrderSortedSign
for on being OperName of SR
for w being Element of the carrier of SR * st ex op being Element of on st w <= the_arity_of op holds
for b₄ being Element of on holds
( b₄ = LBound (on,w) iff for op being Element of on st w <= the_arity_of op holds
b₄ = LBound (op,w) );