let x, y, Y be set ; :: 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 set such that
A1: [x,z] in R and
A2: [z,y] in id Y by Def8;
z = y by A2, Def10;
hence ( y in Y & [x,y] in R ) by A1, A2, Def10; :: thesis: verum

end;

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