:: deftheorem Def10 defines finSigmaFields KOLMOG01:def 10 :
for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for b₅ being Subset-Family of Omega holds
( b₅ = finSigmaFields (F,I) iff for S being Subset of Omega holds
( S in b₅ iff ex E being finite Subset of I st S in sigUn (F,E) ) );