let Y be set ; :: thesis: for x, y being object
for R being Relation holds
( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )
let x, y be object ; :: thesis: for R being Relation holds
( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )
let R be Relation; :: thesis: ( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )
thus ( [x,y] in R * (id Y) implies ( y in Y & [x,y] in R ) ) :: thesis: ( y in Y & [x,y] in R implies [x,y] in R * (id Y) )

proof

assume [x,y] in R * (id Y) ; :: thesis: ( y in Y & [x,y] in R )
then consider z being object such that
A1: [x,z] in R and
A2: [z,y] in id Y by Def6;
z = y by A2, Def8;
hence ( y in Y & [x,y] in R ) by A1, A2, Def8; :: thesis: verum

end;

( y in Y implies [y,y] in id Y ) by Def8;
hence ( y in Y & [x,y] in R implies [x,y] in R * (id Y) ) by Def6; :: thesis: verum