theorem Th11: :: KOLMOG01:11

for Omega, I being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)