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

proof

assume A1: [x,y] in R | X ; :: thesis: [x,y] in R /\ [:X,(rng R):]
then A2: x in X by Def9;
A3: [x,y] in R by A1, Def9;
then y in rng R by XTUPLE_0:def 13;
then [x,y] in [:X,(rng R):] by A2, ZFMISC_1:def 2;
hence [x,y] in R /\ [:X,(rng R):] by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume A4: [x,y] in R /\ [:X,(rng R):] ; :: thesis: [x,y] in R | X
then [x,y] in [:X,(rng R):] by XBOOLE_0:def 4;
then A5: x in X by ZFMISC_1:87;
[x,y] in R by A4, XBOOLE_0:def 4;
hence [x,y] in R | X by A5, Def9; :: thesis: verum