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;
thus LBound (o,w1) has_least_rank_for o,w1 by A1, A2, Def14; :: thesis: verum