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 . A < 1 iff 0 < P . (([#] Sigma) \ A) )

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

for P being Probability of Sigma holds

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

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

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

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

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

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

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

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

for A being Event of Sigma

for P being Probability of Sigma holds

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

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

for P being Probability of Sigma holds

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

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

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

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

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

proof

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

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

then 1 + (- (P . (([#] Sigma) \ A))) < 1 ;

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

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

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

then 1 + (- (P . (([#] Sigma) \ A))) < 1 ;

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

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

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

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

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