for R, Q being Relation st R commutes_with Q holds
R commutes-weakly_with Q