let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; :: thesis: ( T @--> is with_Church-Rosser_property & T @--> is with_UN_property )
set R = T @--> ;
T @--> is locally-confluent

proof

let a, b, c be object ; :: according to REWRITE1:def 24 :: thesis: ( not [a,b] in T @--> or not [a,c] in T @--> or b,c are_convergent_wrt T @--> )
assume that
A1: [a,b] in T @--> and
A2: [a,c] in T @--> ; :: thesis: b,c are_convergent_wrt T @-->
reconsider t = a, t1 = b, t2 = c as type of T by A1, A2, ZFMISC_1:87;
consider a2 being adjective of T such that
not a2 in adjs t1 and
A3: a2 is_properly_applicable_to t1 and
A4: a2 ast t1 = t by A1, Def31;
set tt = t1 "\/" t2;
take t1 "\/" t2 ; :: according to REWRITE1:def 7 :: thesis: ( T @--> reduces b,t1 "\/" t2 & T @--> reduces c,t1 "\/" t2 )
consider a3 being adjective of T such that
not a3 in adjs t2 and
A5: a3 is_properly_applicable_to t2 and
A6: a3 ast t2 = t by A2, Def31;
a3 is_applicable_to t2 by A5;
then t <= t2 by A6, Th20;
then A7: ex B being finite Subset of the adjectives of T st
( B is_properly_applicable_to t1 "\/" t2 & B ast (t1 "\/" t2) = t2 ) by A3, A4, Def30;
a2 is_applicable_to t1 by A3;
then t <= t1 by A4, Th20;
then ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t1 ) by A5, A6, Def30;
hence ( T @--> reduces b,t1 "\/" t2 & T @--> reduces c,t1 "\/" t2 ) by A7, Th72; :: thesis: verum

end;

then T @--> is strongly-normalizing locally-confluent Relation by Th69;
hence ( T @--> is with_Church-Rosser_property & T @--> is with_UN_property ) ; :: thesis: verum