let X be set ; :: thesis: ( X is empty implies X = {} )
assume for x being object holds not x in X ; :: according to XBOOLE_0:def 1 :: thesis: X = {}
then for x being object holds
( x in {} iff x in X ) by XBOOLE_0:def 1;
hence X = {} by TARSKI:2; :: thesis: verum