set d = the Element of D;
take <* the Element of D, the Element of D*> ; :: thesis: ( <* 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 ; :: thesis: not <* the Element of D, the Element of D*> is trivial
thus not <* the Element of D, the Element of D*> is trivial ; :: thesis: verum