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)
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in Y | R iff [x,b] in R * (id Y) )
let 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