let Y be set ; :: thesis: for R being Relation holds Y |` R = R /\ [:(dom R),Y:]
let R be Relation; :: thesis: Y |` R = R /\ [:(dom R),Y:]
set P = R /\ [:(dom R),Y:];
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in Y |` R iff [x,b] in R /\ [:(dom R),Y:] )
let y be object ; :: thesis: ( [x,y] in Y |` R iff [x,y] in R /\ [:(dom R),Y:] )
thus ( [x,y] in Y |` R implies [x,y] in R /\ [:(dom R),Y:] ) :: thesis: ( [x,y] in R /\ [:(dom R),Y:] implies [x,y] in Y |` R )

proof

assume A1: [x,y] in Y |` R ; :: thesis: [x,y] in R /\ [:(dom R),Y:]
then A2: y in Y by Def10;
A3: [x,y] in R by A1, Def10;
then x in dom R by XTUPLE_0:def 12;
then [x,y] in [:(dom R),Y:] by A2, ZFMISC_1:def 2;
hence [x,y] in R /\ [:(dom R),Y:] by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume A4: [x,y] in R /\ [:(dom R),Y:] ; :: thesis: [x,y] in Y |` R
then [x,y] in [:(dom R),Y:] by XBOOLE_0:def 4;
then A5: y in Y by ZFMISC_1:87;
[x,y] in R by A4, XBOOLE_0:def 4;
hence [x,y] in Y |` R by A5, Def10; :: thesis: verum