let R be Relation; :: thesis: ( ( for a, b being object holds not a,b are_critical_wrt R ) implies R is locally-confluent )
assume A1: for a, b being object holds not a,b are_critical_wrt R ; :: thesis: R is locally-confluent
let a, b, c be object ; :: according to REWRITE1:def 24 :: 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 A2: b,c are_divergent<=1_wrt R ;
not b,c are_critical_wrt R by A1;
hence b,c are_convergent_wrt R by A2; :: thesis: verum