let X be set ; :: thesis: id X c= [:X,X:]
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in id X or [x,y] in [:X,X:] )
assume [x,y] in id X ; :: thesis: [x,y] in [:X,X:]
then ( x in X & x = y ) by RELAT_1:def 10;
hence [x,y] in [:X,X:] by ZFMISC_1:87; :: thesis: verum