let T be set ; :: thesis: for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
let F be Subset-Family of T; :: thesis: ( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
thus ( F is SigmaField of T implies ( F is compl-closed & F is closed_for_countable_unions ) ) ; :: thesis: ( F is compl-closed & F is closed_for_countable_unions implies F is SigmaField of T )
assume A1: ( F is compl-closed & F is closed_for_countable_unions ) ; :: thesis: F is SigmaField of T
F is sigma-additive

proof

let M be N_Sub_set_fam of T; :: according to MEASURE1:def 9 :: thesis: ( not M c= F or union M in F )
assume M c= F ; :: thesis: union M in F
hence union M in F by A1, Def4; :: thesis: verum

end;

then reconsider F = F as non empty compl-closed sigma-additive Subset-Family of T by A1;
F is SigmaField of T ;
hence F is SigmaField of T ; :: thesis: verum