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 empty & not <* the Element of D, the Element of D*> is trivial )
len <* the Element of D, the Element of D*> = 2 by FINSEQ_1:61;
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:26
.= <* the Element of D, the Element of D*> /. 1 by FINSEQ_4:26 ;
hence <* the Element of D, the Element of D*> is circular by Def1; :: thesis: ( not <* the Element of D, the Element of D*> is empty & not <* the Element of D, the Element of D*> is trivial )
thus ( not <* the Element of D, the Element of D*> is empty & not <* the Element of D, the Element of D*> is trivial ) ; :: thesis: verum