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