theorem :: REWRITE1:57

for R being Relation holds
( R is confluent iff R [*] is locally-confluent )