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