let R, Q be Relation; ( R commutes_with Q implies R commutes-weakly_with Q )
assume A1:
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 )
; REWRITE1:def 18 R commutes-weakly_with Q
let a, b, c be object ; REWRITE1:def 17 ( [a,b] in R & [a,c] in Q implies ex d being object st
( Q reduces b,d & R reduces c,d ) )
assume
( [a,b] in R & [a,c] in Q )
; ex d being object st
( Q reduces b,d & R reduces c,d )
then
( R reduces a,b & Q reduces a,c )
by Th15;
hence
ex d being object st
( Q reduces b,d & R reduces c,d )
by A1; verum