let X be set ; :: thesis: for D being a_partition of X st D = {} holds
( X is empty & UniCl D = {{}} )
let D be a_partition of X; :: thesis: ( D = {} implies ( X is empty & UniCl D = {{}} ) )
set DU = { (union P) where P is Subset of D : verum } ;
assume A1: D = {} ; :: thesis: ( X is empty & UniCl D = {{}} )
hence X is empty by ZFMISC_1:2, EQREL_1:def 4; :: thesis: UniCl D = {{}}
UniCl D = {{}} by A1, YELLOW_9:16;
hence UniCl D = {{}} ; :: thesis: verum