:: deftheorem Def18 defines commutes_with REWRITE1:def 18 :
for R, Q being Relation holds
( R commutes_with Q iff for a, b, c being object st R reduces a,b & Q reduces a,c holds
ex d being object st
( Q reduces b,d & R reduces c,d ) );