let SR be monotone regular OrderSortedSign; :: thesis: 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; :: thesis: 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 * ; :: thesis: ( w1 <= the_arity_of o implies LBound o,w1 has_least_rank_for o,w1 )
assume A1: w1 <= the_arity_of o ; :: thesis: 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;
o1 has_least_args_for o,w1 by A2, Def12;
hence LBound o,w1 has_least_rank_for o,w1 by A1, A2, Def15; :: thesis: verum