let S be monotone regular OrderSortedSign; :: thesis: 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
let o be OperSymbol of S; :: thesis: for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
LBound (o,w1) <= o
let w1 be Element of the carrier of S * ; :: thesis: ( w1 <= the_arity_of o implies LBound (o,w1) <= o )
assume A1: w1 <= the_arity_of o ; :: thesis: LBound (o,w1) <= o
set lo = LBound (o,w1);
A2: LBound (o,w1) has_least_rank_for o,w1 by A1, Th14;
then LBound (o,w1) has_least_sort_for o,w1 ;
then A3: the_result_sort_of (LBound (o,w1)) <= the_result_sort_of o by A1;
A4: LBound (o,w1) has_least_args_for o,w1 by A2;
then A5: o ~= LBound (o,w1) ;
the_arity_of (LBound (o,w1)) <= the_arity_of o by A1, A4;
hence LBound (o,w1) <= o by A5, A3; :: thesis: verum