let R, Q be Relation; :: thesis: ( R commutes_with Q implies R commutes-weakly_with Q )
assume A1: for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ; :: according to REWRITE1:def 18 :: thesis: R commutes-weakly_with Q
let a, b, c be set ; :: according to REWRITE1:def 17 :: thesis: ( [a,b] in R & [a,c] in Q implies ex d being set st
( Q reduces b,d & R reduces c,d ) )
assume ( [a,b] in R & [a,c] in Q ) ; :: thesis: ex d being set st
( Q reduces b,d & R reduces c,d )
then ( R reduces a,b & Q reduces a,c ) by Th16;
hence ex d being set st
( Q reduces b,d & R reduces c,d ) by A1; :: thesis: verum