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