let Omega be non empty set ; 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; 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 for r, r1 being Real st 0 < r1 holds
r - r1 < rend;
let P be 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 A, B be Event of Sigma; ( 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 )
; 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; verum