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

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