let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Function of Sigma,REAL holds
( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )
let Sigma be SigmaField of Omega; :: thesis: for P being Function of Sigma,REAL holds
( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )
let P be Function of Sigma,REAL ; :: thesis: ( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )
thus ( P is Probability of Sigma implies ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) by Lm2, PROB_1:def 13; :: thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) implies P is Probability of Sigma )
assume that
A1: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) ) and
A2: for ASeq being SetSequence of st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ; :: thesis: P is Probability of Sigma
for ASeq being SetSequence of st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

proof

let ASeq be SetSequence of ; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
assume A3: ASeq is non-ascending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
A4: for A being Event of Sigma holds P . (A ` ) = 1 - (P . A)

proof

let A be Event of Sigma; :: thesis: P . (A ` ) = 1 - (P . A)
reconsider B = A ` as Event of Sigma by PROB_1:50;
A5: A misses B by SUBSET_1:44;
1 = P . ([#] Omega) by A1
.= P . (A \/ B) by SUBSET_1:25
.= (P . A) + (P . B) by A1, A5 ;
hence P . (A ` ) = 1 - (P . A) ; :: thesis: verum

end;

Intersection ASeq = @Intersection ASeq ;
then reconsider V = Intersection ASeq as Event of Sigma ;
set BSeq = @Complement ASeq;
A6: @Complement ASeq is non-descending by A3, Th17;
then A7: P * (@Complement ASeq) is convergent by A2;
Union (@Complement ASeq) = (Intersection ASeq) ` ;
then A8: P . (Union (@Complement ASeq)) = 1 - (P . V) by A4;

A9: now

let n be Element of NAT ; :: thesis: (P * ASeq) . n = 1 - ((P * (@Complement ASeq)) . n)
(P * (@Complement ASeq)) . n = P . ((@Complement ASeq) . n) by FUNCT_2:21
.= P . ((ASeq . n) ` ) by PROB_1:def 4
.= 1 - (P . (ASeq . n)) by A4
.= 1 - ((P * ASeq) . n) by FUNCT_2:21
.= 1 + (- ((P * ASeq) . n)) ;
hence (P * ASeq) . n = 1 - ((P * (@Complement ASeq)) . n) ; :: thesis: verum

end;

hence P * ASeq is convergent by A7, Th5; :: thesis: lim (P * ASeq) = P . (Intersection ASeq)
thus lim (P * ASeq) = 1 - (lim (P * (@Complement ASeq))) by A7, A9, Th5
.= 1 - (1 - (P . V)) by A2, A6, A8
.= P . (Intersection ASeq) ; :: thesis: verum

end;

hence P is Probability of Sigma by A1, PROB_1:def 13; :: thesis: verum