theorem :: REWRITE1:50

for R being Relation holds
( R is confluent iff R commutes_with R )