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

proof

let x, y be set ; :: thesis: ( [x,y] in Y | R iff [x,y] in R * (id Y) )
( [x,y] in Y | R iff ( y in Y & [x,y] in R ) ) by Def12;
hence ( [x,y] in Y | R iff [x,y] in R * (id Y) ) by Th75; :: thesis: verum

end;

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