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

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