let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (@Partial_Union ASeq) is non-decreasing
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (@Partial_Union ASeq) is non-decreasing
let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds P * (@Partial_Union ASeq) is non-decreasing
let P be Probability of Sigma; :: thesis: P * (@Partial_Union ASeq) is non-decreasing
@Partial_Union ASeq is non-descending by Th13;
hence P * (@Partial_Union ASeq) is non-decreasing by Th6; :: thesis: verum