let R be Relation; :: thesis: ( R is confluent implies ( R is locally-confluent & R is with_Church-Rosser_property ) )
assume A2: for a, b being object st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R ; :: according to REWRITE1:def 22 :: thesis: ( R is locally-confluent & R is with_Church-Rosser_property )

hereby :: according to REWRITE1:def 24 :: thesis: R is with_Church-Rosser_property

let a, b, c be object ; :: thesis: ( [a,b] in R & [a,c] in R implies b,c are_convergent_wrt R )
assume ( [a,b] in R & [a,c] in R ) ; :: thesis: b,c are_convergent_wrt R
then ( R reduces a,b & R reduces a,c ) by Th15;
then b,c are_divergent_wrt R ;
hence b,c are_convergent_wrt R by A2; :: thesis: verum

end;

let a, b be object ; :: according to REWRITE1:def 23 :: thesis: ( a,b are_convertible_wrt R implies a,b are_convergent_wrt R )
given p being RedSequence of R \/ (R ~) such that A3: p . 1 = a and
A4: p . (len p) = b ; :: according to REWRITE1:def 3,REWRITE1:def 4 :: thesis: a,b are_convergent_wrt R
defpred S₁[ Nat] means ( c₁ in dom p implies a,p . c₁ are_convergent_wrt R );

now :: thesis: for i being Nat st ( i in dom p implies a,p . i are_convergent_wrt R ) & i + 1 in dom p holds
a,p . (i + 1) are_convergent_wrt R

let i be Nat; :: thesis: ( ( i in dom p implies a,p . i are_convergent_wrt R ) & i + 1 in dom p implies a,p . (b₁ + 1) are_convergent_wrt R )
assume that
A5: ( i in dom p implies a,p . i are_convergent_wrt R ) and
A6: i + 1 in dom p ; :: thesis: a,p . (b₁ + 1) are_convergent_wrt R

per cases ( i in dom p or not i in dom p ) ;

suppose A7: i in dom p ; :: thesis: a,p . (b₁ + 1) are_convergent_wrt R

then consider c being object such that
A8: R reduces a,c and
A9: R reduces p . i,c by A5;
[(p . i),(p . (i + 1))] in R \/ (R ~) by A6, A7, Def2;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in R ~ ) by XBOOLE_0:def 3;
then ( [(p . i),(p . (i + 1))] in R or [(p . (i + 1)),(p . i)] in R ) by RELAT_1:def 7;
then ( R reduces p . i,p . (i + 1) or R reduces p . (i + 1),p . i ) by Th15;
then ( c,p . (i + 1) are_divergent_wrt R or R reduces p . (i + 1),c ) by A9, Th16;
then ( c,p . (i + 1) are_convergent_wrt R or a,p . (i + 1) are_convergent_wrt R ) by A2, A8;
hence a,p . (i + 1) are_convergent_wrt R by A8, Th42; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: a,p . (b₁ + 1) are_convergent_wrt R

then ( i < 0 + 1 or ( i > len p & i + 1 <= len p ) ) by A6, Lm1, Lm3;
then i = 0 by NAT_1:13;
hence a,p . (i + 1) are_convergent_wrt R by A3, Th38; :: thesis: verum

end;

end;

end;

then A10: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A11: len p in dom p by FINSEQ_5:6;
A12: S₁[ 0 ] by Lm1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A12, A10);
hence a,b are_convergent_wrt R by A4, A11; :: thesis: verum