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

proof

assume [x,y] in (id X) * R ; :: thesis: ( x in X & [x,y] in R )
then ex z being object st
( [x,z] in id X & [z,y] in R ) by Def6;
hence ( x in X & [x,y] in R ) by Def8; :: thesis: verum

end;

assume x in X ; :: thesis: ( not [x,y] in R or [x,y] in (id X) * R )
then [x,x] in id X by Def8;
hence ( not [x,y] in R or [x,y] in (id X) * R ) by Def6; :: thesis: verum