theorem :: REWRITE1:56

for R, Q being with_Church-Rosser_property Relation st R commutes_with Q holds
R \/ Q is with_Church-Rosser_property