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