for X being set
for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X