let R, Q be Relation; :: thesis: ( ( 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 ) ) implies for a, b, c being set st Q reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume A2: 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 ) ; :: thesis: for a, b, c being set st Q reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & Q reduces c,d )
let a, b, c be set ; :: thesis: ( Q reduces a,b & R reduces a,c implies ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume ( Q reduces a,b & R reduces a,c ) ; :: 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 A2;
hence ex d being set st
( R reduces b,d & Q reduces c,d ) ; :: thesis: verum