let X be set ; :: thesis: id X c= [:X,X:]
[:X,X:] c= [:X,X:] ;
then reconsider R = [:X,X:] as Relation of X,X ;
for x, y being object st [x,y] in id X holds
[x,y] in R

proof

let x, y be object ; :: thesis: ( [x,y] in id X implies [x,y] in R )
assume [x,y] in id X ; :: thesis: [x,y] in R
then ( x in X & x = y ) by RELAT_1:def 10;
hence [x,y] in R by ZFMISC_1:87; :: thesis: verum

end;

hence id X c= [:X,X:] ; :: thesis: verum