let X be set ; :: thesis: for R being Relation holds R | X = (id X) * R
let R be Relation; :: thesis: R | X = (id X) * R
for x, y being set holds
( [x,y] in R | X iff [x,y] in (id X) * R )

proof

let x, y be set ; :: thesis: ( [x,y] in R | X iff [x,y] in (id X) * R )
( [x,y] in R | X iff ( [x,y] in R & x in X ) ) by Def11;
hence ( [x,y] in R | X iff [x,y] in (id X) * R ) by Th74; :: thesis: verum

end;

hence R | X = (id X) * R by Def2; :: thesis: verum