theorem :: REWRITE1:58

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