for X being set
for S being SigmaField of X
for F being sequence of S holds rng F is N_Sub_set_fam of X