theorem Th23: :: MEASURE1:23
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