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
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 (id X) * R )
let y be object ; :: 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 Def9;
hence ( [x,y] in R | X iff [x,y] in (id X) * R ) by Th42; :: thesis: verum