let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; 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; 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; ( a is_properly_applicable_to t1 & a ast t1 <= radix t2 implies t1 <= radix t2 )
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 = t2 ) } ;
assume that
A1:
a is_properly_applicable_to t1
and
A2:
a ast t1 <= radix t2
; t1 <= radix t2
consider A being finite Subset of the adjectives of T such that
A3:
A is_properly_applicable_to t1 "\/" (radix t2)
and
A4:
A ast (t1 "\/" (radix t2)) = radix t2
by A1, A2, Def30;
consider v1 being FinSequence of the adjectives of T such that
A5:
rng v1 = A
and
A6:
v1 is_properly_applicable_to t1 "\/" (radix t2)
by A3;
T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation
by Th69, Th77;
then
nf (t2,(T @-->)) is_a_normal_form_of t2,T @-->
by REWRITE1:54;
then
T @--> reduces t2, nf (t2,(T @-->))
;
then consider B being finite Subset of the adjectives of T such that
A7:
B is_properly_applicable_to radix t2
and
A8:
t2 = B ast (radix t2)
by Th76;
consider v2 being FinSequence of the adjectives of T such that
A9:
rng v2 = B
and
A10:
v2 is_properly_applicable_to radix t2
by A7;
A11:
rng (v1 ^ v2) = A \/ B
by A5, A9, FINSEQ_1:31;
A12:
radix t2 = v1 ast (t1 "\/" (radix t2))
by A4, A5, A6, Th56, Th57;
then A13:
v1 ^ v2 is_properly_applicable_to t1 "\/" (radix t2)
by A6, A10, Th61;
then A14:
A \/ B is_properly_applicable_to t1 "\/" (radix t2)
by A11;
(A \/ B) ast (t1 "\/" (radix t2)) =
(v1 ^ v2) ast (t1 "\/" (radix t2))
by A11, A13, Th56, Th57
.=
v2 ast (radix t2)
by A12, Th37
.=
t2
by A8, A9, A10, Th56, Th57
;
then
t1 "\/" (radix t2) 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 = t2 ) }
by A14;
then
t1 "\/" (radix t2) <= "\/" ( { 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 = t2 ) } ,T)
by Th80, YELLOW_4:1;
then A15:
t1 "\/" (radix t2) <= radix t2
by Th80;
t1 "\/" (radix t2) >= t1
by YELLOW_0:22;
hence
t1 <= radix t2
by A15, YELLOW_0:def 2; verum