let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds
P . (A \/ B) < 1
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds
P . (A \/ B) < 1
let P be Probability of Sigma; :: thesis: for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds
P . (A \/ B) < 1
let A, B be Event of Sigma; :: thesis: ( A,B are_independent_respect_to P & P . A < 1 & P . B < 1 implies P . (A \/ B) < 1 )
assume that
A1: A,B are_independent_respect_to P and
A2: P . A < 1 and
A3: P . B < 1 ; :: thesis: P . (A \/ B) < 1
A4: ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P by A1, Th38;
A5: 0 < P . (([#] Sigma) \ A) by A2, Th27;
A6: 0 < P . (([#] Sigma) \ B) by A3, Th27;

A7: now

let r, r1 be Real; :: thesis: ( 0 < r1 implies r - r1 < r )
assume 0 < r1 ; :: thesis: r - r1 < r
then - r1 < - 0 by XREAL_1:26;
then r + (- r1) < r + 0 by XREAL_1:8;
hence r - r1 < r ; :: thesis: verum

end;

P . (A \/ B) = 1 - (P . (([#] Sigma) \ (A \/ B))) by Th26
.= 1 - (P . ((([#] Sigma) \ A) /\ (([#] Sigma) \ B))) by XBOOLE_1:53
.= 1 - ((P . (([#] Sigma) \ A)) * (P . (([#] Sigma) \ B))) by A4, Def5 ;
hence P . (A \/ B) < 1 by A5, A6, A7, XREAL_1:131; :: thesis: verum