take <* the Element of D*> ; :: thesis: ( not <* the Element of D*> is empty & <* the Element of D*> is D -valued )
thus ( not <* the Element of D*> is empty & <* the Element of D*> is D -valued ) ; :: thesis: verum