theorem Th21: :: MEASURE1:21
for X being set
for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X