let T be set ; :: thesis: for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
let F be Subset-Family of T; :: thesis: ( F is SigmaField of T implies F is closed_for_countable_unions )
assume A1: F is SigmaField of T ; :: thesis: F is closed_for_countable_unions
let G be countable Subset-Family of T; :: according to TOPGEN_4:def 4 :: thesis: ( G c= F implies union G in F )
assume A2: G c= F ; :: thesis: union G in F
per cases ( G is empty or not G is empty ) ;
suppose G is empty ; :: thesis: union G in F
hence union G in F by A1, PROB_1:4, ZFMISC_1:2; :: thesis: verum
end;
suppose not G is empty ; :: thesis: union G in F
hence union G in F by A1, A2, MEASURE1:def 5; :: thesis: verum
end;
end;