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_Intersection ASeq) is non-increasing

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

let P be Probability of Sigma; :: thesis: P * (Partial_Intersection ASeq) is non-increasing

Partial_Intersection ASeq is V74() by Th10;

hence P * (Partial_Intersection ASeq) is non-increasing by Th7; :: thesis: verum

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

let P be Probability of Sigma; :: thesis: P * (Partial_Intersection ASeq) is non-increasing

Partial_Intersection ASeq is V74() by Th10;

hence P * (Partial_Intersection ASeq) is non-increasing by Th7; :: thesis: verum