let R be Relation; :: thesis: ( R is with_UN_property & R is weakly-normalizing implies R is with_Church-Rosser_property )
assume that
A15: for a, b being object st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b and
A16: for a being object st a in field R holds
a has_a_normal_form_wrt R ; :: according to REWRITE1:def 14,REWRITE1:def 19 :: thesis: R is with_Church-Rosser_property
let a, b be object ; :: according to REWRITE1:def 23 :: thesis: ( a,b are_convertible_wrt R implies a,b are_convergent_wrt R )
assume A17: R \/ (R ~) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: a,b are_convergent_wrt R
A18: field (R \/ (R ~)) = (field R) \/ (field (R ~)) by RELAT_1:18
.= (field R) \/ (field R) by RELAT_1:21
.= field R ;
per cases ( a = b or a <> b ) ;
suppose a = b ; :: thesis: a,b are_convergent_wrt R
hence a,b are_convergent_wrt R by Th38; :: thesis: verum
end;
suppose A19: a <> b ; :: thesis: a,b are_convergent_wrt R
then b in field R by A17, A18, Th18;
then b has_a_normal_form_wrt R by A16;
then consider b9 being object such that
A20: b9 is_a_normal_form_of b,R ;
a in field R by A17, A18, A19, Th18;
then a has_a_normal_form_wrt R by A16;
then consider a9 being object such that
A21: a9 is_a_normal_form_of a,R ;
A22: a9 is_a_normal_form_wrt R by A21;
A23: a,b are_convertible_wrt R by A17;
A24: R reduces a,a9 by A21;
then a9,a are_convertible_wrt R by Th25;
then A25: a9,b are_convertible_wrt R by A23, Th30;
A26: b9 is_a_normal_form_wrt R by A20;
A27: R reduces b,b9 by A20;
then b,b9 are_convertible_wrt R by Th25;
then a9 = b9 by A15, A22, A26, A25, Th30;
hence a,b are_convergent_wrt R by A24, A27; :: thesis: verum
end;
end;