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 )

proof

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;

assume 0 < P . A ; :: thesis: 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