let U be Universe; :: thesis: for X being set st union X is empty holds
X is U -set
let X be set ; :: thesis: ( union X is empty implies X is U -set )
assume union X is empty ; :: thesis: X is U -set

per cases then ( X = {} or X = {{}} ) by ZFMISC_1:33, ZFMISC_1:1, ZFMISC_1:82;

suppose X = {} ; :: thesis: X is U -set

hence X is U -set by CLASSES2:56; :: thesis: verum

end;

suppose X = {{}} ; :: thesis: X is U -set

hence X is U -set by CLASSES2:56, CLASSES2:57; :: thesis: verum

end;

end;