let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; :: thesis: for t being type of T
for X being set st X = { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } holds
( ex_sup_of X,T & radix t = "\/" X,T )
let t be type of T; :: thesis: for X being set st X = { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } holds
( ex_sup_of X,T & radix t = "\/" X,T )
set R = T @--> ;
set AA = { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } ;
A1: T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th70, Th78;
A2: radix t is_>=_than { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) }

proof

let tt be type of T; :: according to LATTICE3:def 9 :: thesis: ( not tt in { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } or tt <= radix t )
assume tt in { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } ; :: thesis: tt <= radix t
then ex t9 being type of T st
( tt = t9 & ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) ) ;
then T @--> reduces t,tt by Th73;
then t,tt are_convertible_wrt T @--> by REWRITE1:26;
then nf t,(T @--> ) = nf tt,(T @--> ) by A1, REWRITE1:56;
then nf t,(T @--> ) is_a_normal_form_of tt,T @--> by A1, REWRITE1:55;
then T @--> reduces tt, nf t,(T @--> ) by REWRITE1:def 6;
hence tt <= radix t by Th68; :: thesis: verum

end;

ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to radix t & A ast (radix t) = t ) by Th77, Th79;
then radix t in { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } ;
then for t9 being type of T st t9 is_>=_than { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } holds
radix t <= t9 by LATTICE3:def 9;
hence for X being set st X = { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } holds
( ex_sup_of X,T & radix t = "\/" X,T ) by A2, YELLOW_0:30; :: thesis: verum