let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of
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
for P being Probability of Sigma holds P * (@Partial_Intersection ASeq) is non-increasing
let ASeq be SetSequence of ; :: 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 non-ascending by Th12;
hence P * (@Partial_Intersection ASeq) is non-increasing by Th7; :: thesis: verum