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 object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in Y |` R iff [x,b] in R * (id Y) )
let y be object ; :: 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 Def10;
hence ( [x,y] in Y |` R iff [x,y] in R * (id Y) ) by Th43; :: thesis: verum