theorem Th5: :: PROB_3:5

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq, BSeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq . n c= BSeq . n holds
(P * ASeq) . n <= (P * BSeq) . n