let S be monotone regular OrderSortedSign; 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; 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 * ; ( w1 <= the_arity_of o implies LBound (o,w1) <= o )
assume A1:
w1 <= the_arity_of o
; 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; verum