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 Def5;
hence X = {} by TARSKI:2; :: thesis: verum