let SR be 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
let o be 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
let w1 be Element of the carrier of SR * ; ( w1 <= the_arity_of o implies LBound (o,w1) has_least_rank_for o,w1 )
assume A1:
w1 <= the_arity_of o
; LBound (o,w1) has_least_rank_for o,w1
then consider o1 being OperSymbol of SR such that
A2:
o1 has_least_rank_for o,w1
by Th11;
thus
LBound (o,w1) has_least_rank_for o,w1
by A1, A2, Def14; verum