:: deftheorem Def12 defines with_proper_subsets SETFAM_1:def 12 :
for X being set
for F being Subset-Family of X holds
( F is with_proper_subsets iff not X in F );