let x be object ; :: thesis: id {x} = {[x,x]}
x in {x} by TARSKI:def 1;
then [x,x] in id {x} by RELAT_1:def 10;
then A1: {[x,x]} c= id {x} by ZFMISC_1:31;
[:{x},{x}:] = {[x,x]} by ZFMISC_1:29;
then id {x} c= {[x,x]} by Lm2;
hence id {x} = {[x,x]} by A1; :: thesis: verum