let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; :: thesis: for t1, t2 being type of T
for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= radix t2 holds
t1 <= radix t2
let t1, t2 be type of T; :: thesis: for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= radix t2 holds
t1 <= radix t2
let a be adjective of T; :: thesis: ( a is_properly_applicable_to t1 & a ast t1 <= radix t2 implies t1 <= radix t2 )
set R = T @--> ;
A1: T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th70, Th78;
set AA = { t' where t' is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t' & A ast t' = t2 ) } ;
assume ( a is_properly_applicable_to t1 & a ast t1 <= radix t2 ) ; :: thesis: t1 <= radix t2
then consider A being finite Subset of the adjectives of T such that
A2: ( A is_properly_applicable_to t1 "\/" (radix t2) & A ast (t1 "\/" (radix t2)) = radix t2 ) by Def30;
nf t2,(T @--> ) is_a_normal_form_of t2,T @--> by A1, REWRITE1:55;
then T @--> reduces t2, nf t2,(T @--> ) by REWRITE1:def 6;
then consider B being finite Subset of the adjectives of T such that
A3: ( B is_properly_applicable_to radix t2 & t2 = B ast (radix t2) ) by Th77;
consider v1 being FinSequence of the adjectives of T such that
A4: ( rng v1 = A & v1 is_properly_applicable_to t1 "\/" (radix t2) ) by A2, Def29;
consider v2 being FinSequence of the adjectives of T such that
A5: ( rng v2 = B & v2 is_properly_applicable_to radix t2 ) by A3, Def29;
A6: rng (v1 ^ v2) = A \/ B by A4, A5, FINSEQ_1:44;
A7: radix t2 = v1 ast (t1 "\/" (radix t2)) by A2, A4, Th57, Th58;
then v1 ^ v2 is_properly_applicable_to t1 "\/" (radix t2) by A4, A5, Th62;
then A8: ( A \/ B is_properly_applicable_to t1 "\/" (radix t2) & v1 ^ v2 is_applicable_to t1 "\/" (radix t2) ) by A6, Def29, Th58;
then (A \/ B) ast (t1 "\/" (radix t2)) = (v1 ^ v2) ast (t1 "\/" (radix t2)) by A6, Th57
.= v2 ast (radix t2) by A7, Th38
.= t2 by A3, A5, Th57, Th58 ;
then ( t1 "\/" (radix t2) in { t' where t' is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t' & A ast t' = t2 ) } & ex_sup_of { t' where t' is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t' & A ast t' = t2 ) } ,T ) by A8, Th81;
then t1 "\/" (radix t2) <= "\/" { t' where t' is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t' & A ast t' = t2 ) } ,T by YELLOW_4:1;
then ( t1 "\/" (radix t2) <= radix t2 & t1 "\/" (radix t2) >= t1 ) by Th81, YELLOW_0:22;
hence t1 <= radix t2 by YELLOW_0:def 2; :: thesis: verum