for T being set
for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )