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