theorem :: BOR_CANT:19

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, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)