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 Th69, Th77;
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 Th72;
then t,tt are_convertible_wrt T @--> by REWRITE1:25;
then nf (t,(T @-->)) = nf (tt,(T @-->)) by A1, REWRITE1:55;
then nf (t,(T @-->)) is_a_normal_form_of tt,T @--> by A1, REWRITE1:54;
then T @--> reduces tt, nf (t,(T @-->)) ;
hence tt <= radix t by Th67; :: 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 Th76, Th78;
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 ;
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