let X be set ; :: thesis: for S being SigmaField of X
for F being sequence of S holds union (rng F) is Element of S
let S be SigmaField of X; :: thesis: for F being sequence of S holds union (rng F) is Element of S
let F be sequence of S; :: thesis: union (rng F) is Element of S
( rng F is N_Sub_set_fam of X & rng F c= S ) by Th23, RELAT_1:def 19;
hence union (rng F) is Element of S by Def5; :: thesis: verum