now :: thesis: not id D = {}

hence
not id D is empty
; :: thesis: verumset 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;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