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 by A1;
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