let R, Q be Relation; :: thesis: ( ( 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 ) ) implies for a, b, c being object st [a,b] in Q & [a,c] in R holds
ex d being object st
( R reduces b,d & Q reduces c,d ) )
assume A1: 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 ) ; :: thesis: for a, b, c being object st [a,b] in Q & [a,c] in R holds
ex d being object st
( R reduces b,d & Q reduces c,d )
let a, b, c be object ; :: thesis: ( [a,b] in Q & [a,c] in R implies ex d being object st
( R reduces b,d & Q reduces c,d ) )
assume ( [a,b] in Q & [a,c] in R ) ; :: thesis: ex d being object st
( R reduces b,d & Q reduces c,d )
then ex d being object st
( Q reduces c,d & R reduces b,d ) by A1;
hence ex d being object st
( R reduces b,d & Q reduces c,d ) ; :: thesis: verum