:: deftheorem defines sigma PROB_1:def 9 :
for Omega being non empty set
for X being Subset-Family of Omega
for b₃ being SigmaField of Omega holds
( b₃ = sigma X iff ( X c= b₃ & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b₃ c= Z ) ) );