let R, Q be Relation; :: thesis: ( ( for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) implies for a, b, c being set st [a,b] in Q & [a,c] in R holds
ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume A1: for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ; :: thesis: for a, b, c being set st [a,b] in Q & [a,c] in R holds
ex d being set st
( R reduces b,d & Q reduces c,d )
let a, b, c be set ; :: thesis: ( [a,b] in Q & [a,c] in R implies ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume ( [a,b] in Q & [a,c] in R ) ; :: thesis: ex d being set st
( R reduces b,d & Q reduces c,d )
then ex d being set st
( Q reduces c,d & R reduces b,d ) by A1;
hence ex d being set st
( R reduces b,d & Q reduces c,d ) ; :: thesis: verum