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
A1: now :: thesis: for r, r1 being Real st 0 < r1 holds
r - r1 < r
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:24;
then r + (- r1) < r + 0 by XREAL_1:6;
hence r - r1 < r ; :: thesis: verum
end;
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
A2: A,B are_independent_respect_to P and
A3: ( P . A < 1 & P . B < 1 ) ; :: thesis: P . (A \/ B) < 1
A4: ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P by A2, Th26;
A5: ( 0 < P . (([#] Sigma) \ A) & 0 < P . (([#] Sigma) \ B) ) by A3, Th17;
P . (A \/ B) = 1 - (P . (([#] Sigma) \ (A \/ B))) by Th16
.= 1 - (P . ((([#] Sigma) \ A) /\ (([#] Sigma) \ B))) by XBOOLE_1:53
.= 1 - ((P . (([#] Sigma) \ A)) * (P . (([#] Sigma) \ B))) by A4 ;
hence P . (A \/ B) < 1 by A5, A1, XREAL_1:129; :: thesis: verum