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

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