let X be set ; :: thesis: ( not union X = {} or X = {} or X = {{}} )
assume A: union X = {} ; :: thesis: ( X = {} or X = {{}} )
assume X <> {} ; :: thesis: X = {{}}
then consider x being set such that
B: x in X by XBOOLE_0:def 1;
thus X = {{}} :: thesis: verum

proof

thus X c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in {{}} )
assume a in X ; :: thesis: a in {{}}
then a = {} by A, ORDERS_1:6;
hence a in {{}} by TARSKI:def 1; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {{}} or a in X )
assume a in {{}} ; :: thesis: a in X
then a = {} by TARSKI:def 1;
hence a in X by B, A, ORDERS_1:6; :: thesis: verum

end;