theorem :: REWRITE1:52

for R being Relation holds
( R is locally-confluent iff R commutes-weakly_with R )