theorem Th14: :: OSALG_1: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
LBound (o,w1) has_least_rank_for o,w1