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