let X be set ; :: thesis: id X c= [:X,X:]
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in id X or [x,b₁] in [:X,X:] )
let y be set ; :: 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