set d = the Element of D;
take <* the Element of D*> ; :: thesis: ( <* the Element of D*> is circular & not <* the Element of D*> is empty & <* the Element of D*> is trivial )
<* the Element of D*> /. 1 = <* the Element of D*> /. (len <* the Element of D*>) by FINSEQ_1:56;
hence <* the Element of D*> is circular by Def1; :: thesis: ( not <* the Element of D*> is empty & <* the Element of D*> is trivial )
thus ( not <* the Element of D*> is empty & <* the Element of D*> is trivial ) ; :: thesis: verum