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