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) )
A1: ( [x,y] in R | X iff ( [x,y] in R & x in X ) ) by Def11;
A2: ( [x,y] in R | (X /\ Y) iff ( [x,y] in R & x in X /\ Y ) ) by Def11;
( [x,y] in (R | X) | Y iff ( [x,y] in R | X & x in Y ) ) by Def11;
hence ( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) ) by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

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