let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Event of Sigma holds
( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A being Event of Sigma holds
( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )
let P be Probability of Sigma; :: thesis: for A being Event of Sigma holds
( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )
let A be Event 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 P . A < 1 ; :: thesis: 0 < P . (([#] Sigma) \ A)
then 1 - (P . (([#] Sigma) \ A)) < 1 by Th26;
then 1 + (- (P . (([#] Sigma) \ A))) < 1 ;
then - (P . (([#] Sigma) \ A)) < 1 - 1 by XREAL_1:22;
then 0 < - (- (P . (([#] Sigma) \ A))) ;
hence 0 < P . (([#] Sigma) \ A) ; :: thesis: verum

end;

assume 0 < P . (([#] Sigma) \ A) ; :: thesis: P . A < 1
then 0 < 1 - (P . A) by PROB_1:68;
then (P . A) + 0 < 1 by XREAL_1:22;
hence P . A < 1 ; :: thesis: verum