let R be Relation; :: thesis: ( R is with_UN_property & R is weakly-normalizing implies R is with_Church-Rosser_property )
assume that
A16: for a, b being set 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
A17: for a being set 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 set ; :: according to REWRITE1:def 23 :: thesis: ( a,b are_convertible_wrt R implies a,b are_convergent_wrt R )
assume A18: R \/ (R ~) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: a,b are_convergent_wrt R
A19: field (R \/ (R ~)) = (field R) \/ (field (R ~)) by RELAT_1:33
.= (field R) \/ (field R) by RELAT_1:38
.= 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 Th39; :: thesis: verum

end;

suppose A20: a <> b ; :: thesis: a,b are_convergent_wrt R

then b in field R by A18, A19, Th19;
then b has_a_normal_form_wrt R by A17;
then consider b9 being set such that
A21: b9 is_a_normal_form_of b,R by Def11;
a in field R by A18, A19, A20, Th19;
then a has_a_normal_form_wrt R by A17;
then consider a9 being set such that
A22: a9 is_a_normal_form_of a,R by Def11;
A23: a9 is_a_normal_form_wrt R by A22, Def6;
A24: a,b are_convertible_wrt R by A18, Def4;
A25: R reduces a,a9 by A22, Def6;
then a9,a are_convertible_wrt R by Th26;
then A26: a9,b are_convertible_wrt R by A24, Th31;
A27: b9 is_a_normal_form_wrt R by A21, Def6;
A28: R reduces b,b9 by A21, Def6;
then b,b9 are_convertible_wrt R by Th26;
then a9 = b9 by A16, A23, A27, A26, Th31;
hence a,b are_convergent_wrt R by A25, A28, Def7; :: thesis: verum

end;

end;