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

( 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