now :: thesis: not id D = {}
set y = the Element of D;
A1: [ the Element of D, the Element of D] 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