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