set d = the Element of D;
take <* the Element of D*> ; :: thesis: ( <* the Element of D*> is circular & <* the Element of D*> is 1 -element )
thus <* the Element of D*> is circular by FINSEQ_1:39; :: thesis: <* the Element of D*> is 1 -element
thus <* the Element of D*> is 1 -element ; :: thesis: verum