:: deftheorem defines locally-confluent REWRITE1:def 24 :
for R being Relation holds
( R is locally-confluent iff for a, b, c being object st [a,b] in R & [a,c] in R holds
b,c are_convergent_wrt R );