set x = the Element of D;
( <* the Element of D*> in D * & not <* the Element of D*> in {{}} ) by TARSKI:def 1, FINSEQ_1:def 11;
hence not (D *) \ {{}} is empty by XBOOLE_0:def 5; :: thesis: verum