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
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in Y | (X | R) iff [x,b] in (Y /\ X) | R )
let 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