let R be Relation; :: thesis: ( R is with_Church-Rosser_property implies R is confluent )
assume A1: for a, b being object st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R ; :: according to REWRITE1:def 23 :: thesis: R is confluent
let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
assume a,b are_divergent_wrt R ; :: thesis: a,b are_convergent_wrt R
then a,b are_convertible_wrt R by Th37;
hence a,b are_convergent_wrt R by A1; :: thesis: verum