:: deftheorem Def8 defines with_non-empty_elements SETFAM_1:def 8 :
for IT being set holds
( IT is with_non-empty_elements iff not {} in IT );