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

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