theorem Th4: :: BOR_CANT:4

for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n