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