let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma

for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

let P be Probability of Sigma; :: thesis: ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

thus ( P . (([#] Sigma) \ A) < 1 implies 0 < P . A ) :: thesis: ( 0 < P . A implies P . (([#] Sigma) \ A) < 1 )

then 0 < 1 - (P . (([#] Sigma) \ A)) by Th16;

then (P . (([#] Sigma) \ A)) + 0 < 1 by XREAL_1:20;

hence P . (([#] Sigma) \ A) < 1 ; :: thesis: verum

for A being Event of Sigma

for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma

for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

let P be Probability of Sigma; :: thesis: ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

thus ( P . (([#] Sigma) \ A) < 1 implies 0 < P . A ) :: thesis: ( 0 < P . A implies P . (([#] Sigma) \ A) < 1 )

proof

assume
0 < P . A
; :: thesis: P . (([#] Sigma) \ A) < 1
assume
P . (([#] Sigma) \ A) < 1
; :: thesis: 0 < P . A

then 1 - (P . A) < 1 by PROB_1:32;

then 1 + (- (P . A)) < 1 ;

then - (P . A) < 1 - 1 by XREAL_1:20;

hence 0 < P . A ; :: thesis: verum

end;then 1 - (P . A) < 1 by PROB_1:32;

then 1 + (- (P . A)) < 1 ;

then - (P . A) < 1 - 1 by XREAL_1:20;

hence 0 < P . A ; :: thesis: verum

then 0 < 1 - (P . (([#] Sigma) \ A)) by Th16;

then (P . (([#] Sigma) \ A)) + 0 < 1 by XREAL_1:20;

hence P . (([#] Sigma) \ A) < 1 ; :: thesis: verum