set d = the Element of D;
take
<* the Element of D, the Element of D*>
; ( <* the Element of D, the Element of D*> is circular & not <* the Element of D, the Element of D*> is trivial )
len <* the Element of D, the Element of D*> = 2
by FINSEQ_1:44;
then <* the Element of D, the Element of D*> /. (len <* the Element of D, the Element of D*>) =
the Element of D
by FINSEQ_4:17
.=
<* the Element of D, the Element of D*> /. 1
by FINSEQ_4:17
;
hence
<* the Element of D, the Element of D*> is circular
; not <* the Element of D, the Element of D*> is trivial
thus
not <* the Element of D, the Element of D*> is trivial
; verum