:: deftheorem Def1 defines compl-closed PROB_1:def 1 :
for X being set
for IT being Subset-Family of X holds
( IT is compl-closed iff for A being Subset of X st A in IT holds
A ` in IT );