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