:: deftheorem Def10 defines empty-membered SETFAM_1:def 10 :
for E being set holds
( E is empty-membered iff for x being non empty set holds not x in E );