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

proof

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

end;

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