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

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

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 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 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;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

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