theorem Th3: :: PROB_2:3

for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for B being Event of Sigma ex BSeq being SetSequence of Sigma st
for n being Nat holds BSeq . n = (ASeq . n) /\ B