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 by Def12;
then A3: the_result_sort_of (LBound o,w1) <= the_result_sort_of o by A1, Def11;
A4: LBound o,w1 has_least_args_for o,w1 by A2, Def12;
then A5: o ~= LBound o,w1 by Def10;
the_arity_of (LBound o,w1) <= the_arity_of o by A1, A4, Def10;
hence LBound o,w1 <= o by A5, A3, Def22; :: thesis: verum