:: deftheorem Def9 defines MeetSections KOLMOG01:def 9 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty set
for J being non empty Subset of I
for F being ManySortedSigmaField of I,Sigma
for b₆ being Subset-Family of Omega holds
( b₆ = MeetSections (J,F) iff for x being Subset of Omega holds
( x in b₆ iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) );