now

consider y being Element of D;
A1: [y,y] in id D by RELAT_1:def 10;
assume id D = {} ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum

end;

hence not id D is empty ; :: thesis: verum