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

end;

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