set x = the Element of D;
take <* the Element of D*> ; :: thesis: not <* the Element of D*> is empty
thus not <* the Element of D*> is empty ; :: thesis: verum