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