{} in U1 by Th56;
then reconsider x = bool {} as Element of U1 by Th59;
take x ; :: thesis: not x is empty
thus not x is empty ; :: thesis: verum