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):]
reconsider P = R /\ [:X,(rng R):] as Relation ;
for x, y being set holds
( [x,y] in R | X iff [x,y] in P )

proof

let x, y be set ; :: thesis: ( [x,y] in R | X iff [x,y] in P )
thus ( [x,y] in R | X implies [x,y] in P ) :: thesis: ( [x,y] in P implies [x,y] in R | X )

proof

assume A1: [x,y] in R | X ; :: thesis: [x,y] in P
then A2: x in X by Def11;
A3: [x,y] in R by A1, Def11;
then y in rng R by Def5;
then [x,y] in [:X,(rng R):] by A2, ZFMISC_1:def 2;
hence [x,y] in P by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume A4: [x,y] in P ; :: 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:106;
[x,y] in R by A4, XBOOLE_0:def 4;
hence [x,y] in R | X by A5, Def11; :: thesis: verum

end;

hence R | X = R /\ [:X,(rng R):] by Def2; :: thesis: verum