consider d being Element of D;
reconsider e = <*d*> as Element of D * by FINSEQ_1:def 11;
take e ; :: thesis: not e is empty
thus not e is empty ; :: thesis: verum