theorem Th51: :: REWRITE1:51

for R being Relation holds
( R is confluent iff for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )