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 set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in Y | R iff [x,b] in R /\ [:(dom R),Y:] )
let y be set ; :: 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 Def12;
A3: [x,y] in R by A1, Def12;
then x in dom R by Def4;
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, Def12; :: thesis: verum