now :: thesis: for x being object holds not x in union {}

given x being object such that A1: x in union {} ; :: thesis: contradiction
ex X being set st
( x in X & X in {} ) by A1, TARSKI:def 4;
hence contradiction ; :: thesis: verum

end;

hence union {} = {} by XBOOLE_0:7; :: thesis: verum