:: deftheorem Def1 defines empty XBOOLE_0:def 1 :
for X being set holds
( X is empty iff for x being object holds not x in X );