let X, Y be set ; :: thesis: for R being Relation holds (R | X) | Y = R | (X /\ Y)
let R be Relation; :: thesis: (R | X) | Y = R | (X /\ Y)
for x, y being set holds
( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) )

proof

let x, y be set ; :: thesis: ( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) )
( ( [x,y] in (R | X) | Y implies ( [x,y] in R | X & x in Y ) ) & ( [x,y] in R | X & x in Y implies [x,y] in (R | X) | Y ) & ( [x,y] in R | X implies ( [x,y] in R & x in X ) ) & ( [x,y] in R & x in X implies [x,y] in R | X ) & ( [x,y] in R | (X /\ Y) implies ( [x,y] in R & x in X /\ Y ) ) & ( [x,y] in R & x in X /\ Y implies [x,y] in R | (X /\ Y) ) & ( x in X /\ Y implies ( x in X & x in Y ) ) & ( x in X & x in Y implies x in X /\ Y ) ) by Def11, XBOOLE_0:def 4;
hence ( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) ) ; :: thesis: verum

end;

hence (R | X) | Y = R | (X /\ Y) by Def2; :: thesis: verum