:: deftheorem defines commutes-weakly_with REWRITE1:def 17 :
for R, Q being Relation holds
( R commutes-weakly_with Q iff for a, b, c being object st [a,b] in R & [a,c] in Q holds
ex d being object st
( Q reduces b,d & R reduces c,d ) );