let R be Relation; :: thesis: ( ( for a, b being set holds not a,b are_critical_wrt R ) implies R is locally-confluent )
assume A1: for a, b being set holds not a,b are_critical_wrt R ; :: thesis: R is locally-confluent
let a, b, c be set ; :: 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 ( b,c are_divergent<=1_wrt R & not b,c are_critical_wrt R ) by A1, Def10;
hence b,c are_convergent_wrt R by Def27; :: thesis: verum