let X be set ; :: thesis: for S being SigmaField of X
for F being sequence of S holds rng F is N_Sub_set_fam of X
let S be SigmaField of X; :: thesis: for F being sequence of S holds rng F is N_Sub_set_fam of X
let F be sequence of S; :: thesis: rng F is N_Sub_set_fam of X
ex H being sequence of (bool X) st rng F = rng H
proof
rng F c= bool X ;
then reconsider F = F as sequence of (bool X) by FUNCT_2:6;
take F ; :: thesis: rng F = rng F
thus rng F = rng F ; :: thesis: verum
end;
hence rng F is N_Sub_set_fam of X by SUPINF_2:def 8; :: thesis: verum