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)
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in (R | X) | Y iff [x,b] in R | (X /\ Y) )
let y be object ; :: 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 Def9;
A2: ( [x,y] in R | (X /\ Y) iff ( [x,y] in R & x in X /\ Y ) ) by Def9;
( [x,y] in (R | X) | Y iff ( [x,y] in R | X & x in Y ) ) by Def9;
hence ( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) ) by A1, A2, XBOOLE_0:def 4; :: thesis: verum