{} c= D ;
then union {} in { (union P) where P is Subset of D : verum } ;
hence UniCl D is with_empty_element by ZFMISC_1:2, Th14; :: thesis: verum