consider d being Element of D;
take <*d*> ; :: thesis: ( <*d*> is circular & not <*d*> is empty & <*d*> is trivial )
thus <*d*> is circular :: thesis: ( not <*d*> is empty & <*d*> is trivial )

proof

thus <*d*> /. 1 = <*d*> /. (len <*d*>) by FINSEQ_1:56; :: according to FINSEQ_6:def 1 :: thesis: verum

end;

thus ( not <*d*> is empty & <*d*> is trivial ) ; :: thesis: verum