theorem :: OSALG_1:35

for S being monotone regular OrderSortedSign
for o being OperSymbol of S
for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
LBound (o,w1) <= o