theorem Th7: :: PROB_4:7

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )