let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for Prob being Probability of Sigma

for A being SetSequence of Sigma holds

( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma holds

( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma holds

( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

let A be SetSequence of Sigma; :: thesis: ( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

thus A1: lim_sup A = @lim_sup A :: thesis: ( lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

for Prob being Probability of Sigma

for A being SetSequence of Sigma holds

( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma holds

( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma holds

( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

let A be SetSequence of Sigma; :: thesis: ( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

thus A1: lim_sup A = @lim_sup A :: thesis: ( lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )

proof

A18:
for A being SetSequence of Sigma holds lim_inf A = @lim_inf A
A2:
for n being Nat

for x being set holds

( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st

( k >= n & x in A . k ) )

( ( for m being Nat ex n being Nat st

( n >= m & x in A . n ) ) iff for m being Nat ex n being Nat st x in A . (m + n) )

( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st x in A . (m + n) )

( x in lim_sup A iff x in @Intersection (Union_Shift_Seq A) )

end;for x being set holds

( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st

( k >= n & x in A . k ) )

proof

A10:
for x being object holds
let n be Nat; :: thesis: for x being set holds

( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st

( k >= n & x in A . k ) )

let x be set ; :: thesis: ( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st

( k >= n & x in A . k ) )

( k >= n & x in A . k ) ; :: thesis: ex k being Nat st x in (A ^\ n) . k

then consider k being Nat such that

A7: ( k >= n & x in A . k ) ;

consider knat being Nat such that

A8: k = n + knat by A7, NAT_1:10;

reconsider knat = knat as Nat ;

A9: ( x in A . k implies x in (A ^\ n) . knat ) by A8, NAT_1:def 3;

thus ex k being Nat st x in (A ^\ n) . k by A7, A9; :: thesis: verum

end;( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st

( k >= n & x in A . k ) )

let x be set ; :: thesis: ( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st

( k >= n & x in A . k ) )

hereby :: thesis: ( ex k being Nat st

( k >= n & x in A . k ) implies ex k being Nat st x in (A ^\ n) . k )

assume
ex k being Nat st ( k >= n & x in A . k ) implies ex k being Nat st x in (A ^\ n) . k )

assume
ex k being Nat st x in (A ^\ n) . k
; :: thesis: ex k being Nat st

( k >= n & x in A . k )

then consider k being Nat such that

A3: x in (A ^\ n) . k ;

A4: x in A . (k + n) by A3, NAT_1:def 3;

consider k being Nat such that

A5: x in A . (k + n) by A4;

consider k being Nat such that

A6: ( k >= n & x in A . k ) by A5, NAT_1:11;

thus ex k being Nat st

( k >= n & x in A . k ) by A6; :: thesis: verum

end;( k >= n & x in A . k )

then consider k being Nat such that

A3: x in (A ^\ n) . k ;

A4: x in A . (k + n) by A3, NAT_1:def 3;

consider k being Nat such that

A5: x in A . (k + n) by A4;

consider k being Nat such that

A6: ( k >= n & x in A . k ) by A5, NAT_1:11;

thus ex k being Nat st

( k >= n & x in A . k ) by A6; :: thesis: verum

( k >= n & x in A . k ) ; :: thesis: ex k being Nat st x in (A ^\ n) . k

then consider k being Nat such that

A7: ( k >= n & x in A . k ) ;

consider knat being Nat such that

A8: k = n + knat by A7, NAT_1:10;

reconsider knat = knat as Nat ;

A9: ( x in A . k implies x in (A ^\ n) . knat ) by A8, NAT_1:def 3;

thus ex k being Nat st x in (A ^\ n) . k by A7, A9; :: thesis: verum

( ( for m being Nat ex n being Nat st

( n >= m & x in A . n ) ) iff for m being Nat ex n being Nat st x in A . (m + n) )

proof

A15:
for x being object holds
let x be object ; :: thesis: ( ( for m being Nat ex n being Nat st

( n >= m & x in A . n ) ) iff for m being Nat ex n being Nat st x in A . (m + n) )

( n >= m & x in A . n )

thus for m being Nat ex n being Nat st

( n >= m & x in A . n ) :: thesis: verum

end;( n >= m & x in A . n ) ) iff for m being Nat ex n being Nat st x in A . (m + n) )

hereby :: thesis: ( ( for m being Nat ex n being Nat st x in A . (m + n) ) implies for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

assume A13:
for m being Nat ex n being Nat st x in A . (m + n)
; :: thesis: for m being Nat ex n being Nat st ( n >= m & x in A . n ) )

assume A11:
for m being Nat ex n being Nat st

( n >= m & x in A . n ) ; :: thesis: for m being Nat ex n being Nat st x in A . (m + n)

thus for m being Nat ex n being Nat st x in A . (m + n) :: thesis: verum

end;( n >= m & x in A . n ) ; :: thesis: for m being Nat ex n being Nat st x in A . (m + n)

thus for m being Nat ex n being Nat st x in A . (m + n) :: thesis: verum

( n >= m & x in A . n )

thus for m being Nat ex n being Nat st

( n >= m & x in A . n ) :: thesis: verum

( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st x in A . (m + n) )

proof

for x being object holds
let x be object ; :: thesis: ( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st x in A . (m + n) )

then for m being Nat ex n being Nat st

( n >= m & x in A . n ) by A10;

hence x in @Intersection (Union_Shift_Seq A) by Th14; :: thesis: verum

end;hereby :: thesis: ( ( for m being Nat ex n being Nat st x in A . (m + n) ) implies x in @Intersection (Union_Shift_Seq A) )

assume
for m being Nat ex n being Nat st x in A . (m + n)
; :: thesis: x in @Intersection (Union_Shift_Seq A)assume
x in @Intersection (Union_Shift_Seq A)
; :: thesis: for m being Nat ex n being Nat st x in A . (m + n)

then A16: for m being Nat ex n being Nat st

( n >= m & x in A . n ) by Th14;

thus for m being Nat ex n being Nat st x in A . (m + n) by A16, A10; :: thesis: verum

end;then A16: for m being Nat ex n being Nat st

( n >= m & x in A . n ) by Th14;

thus for m being Nat ex n being Nat st x in A . (m + n) by A16, A10; :: thesis: verum

then for m being Nat ex n being Nat st

( n >= m & x in A . n ) by A10;

hence x in @Intersection (Union_Shift_Seq A) by Th14; :: thesis: verum

( x in lim_sup A iff x in @Intersection (Union_Shift_Seq A) )

proof

hence
lim_sup A = @lim_sup A
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in lim_sup A iff x in @Intersection (Union_Shift_Seq A) )

then for m being Nat ex n being Nat st x in A . (m + n) by A15;

hence x in lim_sup A by SETLIM_1:66; :: thesis: verum

end;hereby :: thesis: ( x in @Intersection (Union_Shift_Seq A) implies x in lim_sup A )

assume
x in @Intersection (Union_Shift_Seq A)
; :: thesis: x in lim_sup Aassume
x in lim_sup A
; :: thesis: x in @Intersection (Union_Shift_Seq A)

then A17: for m being Nat ex n being Nat st x in A . (m + n) by SETLIM_1:66;

thus x in @Intersection (Union_Shift_Seq A) by A17, A15; :: thesis: verum

end;then A17: for m being Nat ex n being Nat st x in A . (m + n) by SETLIM_1:66;

thus x in @Intersection (Union_Shift_Seq A) by A17, A15; :: thesis: verum

then for m being Nat ex n being Nat st x in A . (m + n) by A15;

hence x in lim_sup A by SETLIM_1:66; :: thesis: verum

proof

A23:
@lim_inf (Complement A) = (@lim_sup A) `
let A be SetSequence of Sigma; :: thesis: lim_inf A = @lim_inf A

A19: for x being object holds

( ex n being Nat st

for k being Nat st k >= n holds

x in A . k iff ex n being Nat st

for k being Nat holds x in A . (n + k) )

( x in @lim_inf A iff x in lim_inf A )

end;A19: for x being object holds

( ex n being Nat st

for k being Nat st k >= n holds

x in A . k iff ex n being Nat st

for k being Nat holds x in A . (n + k) )

proof

for x being object holds
let x be object ; :: thesis: ( ex n being Nat st

for k being Nat st k >= n holds

x in A . k iff ex n being Nat st

for k being Nat holds x in A . (n + k) )

for k being Nat holds x in A . (n + k) ; :: thesis: ex n being Nat st

for k being Nat st k >= n holds

x in A . k

then consider n being Nat such that

A21: for k being Nat holds x in A . (n + k) ;

for k being Nat st k >= n holds

x in A . k

for k being Nat st k >= n holds

x in A . k ; :: thesis: verum

end;for k being Nat st k >= n holds

x in A . k iff ex n being Nat st

for k being Nat holds x in A . (n + k) )

hereby :: thesis: ( ex n being Nat st

for k being Nat holds x in A . (n + k) implies ex n being Nat st

for k being Nat st k >= n holds

x in A . k )

assume
ex n being Nat st for k being Nat holds x in A . (n + k) implies ex n being Nat st

for k being Nat st k >= n holds

x in A . k )

assume
ex n being Nat st

for k being Nat st k >= n holds

x in A . k ; :: thesis: ex n being Nat st

for k being Nat holds x in A . (n + k)

then consider n being Nat such that

A20: for k being Nat st k >= n holds

x in A . k ;

for k being Nat holds x in A . (n + k) by A20, NAT_1:11;

hence ex n being Nat st

for k being Nat holds x in A . (n + k) ; :: thesis: verum

end;for k being Nat st k >= n holds

x in A . k ; :: thesis: ex n being Nat st

for k being Nat holds x in A . (n + k)

then consider n being Nat such that

A20: for k being Nat st k >= n holds

x in A . k ;

for k being Nat holds x in A . (n + k) by A20, NAT_1:11;

hence ex n being Nat st

for k being Nat holds x in A . (n + k) ; :: thesis: verum

for k being Nat holds x in A . (n + k) ; :: thesis: ex n being Nat st

for k being Nat st k >= n holds

x in A . k

then consider n being Nat such that

A21: for k being Nat holds x in A . (n + k) ;

for k being Nat st k >= n holds

x in A . k

proof

hence
ex n being Nat st
let k be Nat; :: thesis: ( k >= n implies x in A . k )

assume n <= k ; :: thesis: x in A . k

then consider knat being Nat such that

A22: k = n + knat by NAT_1:10;

reconsider knat = knat as Nat ;

x in A . (n + knat) by A21;

hence x in A . k by A22; :: thesis: verum

end;assume n <= k ; :: thesis: x in A . k

then consider knat being Nat such that

A22: k = n + knat by NAT_1:10;

reconsider knat = knat as Nat ;

x in A . (n + knat) by A21;

hence x in A . k by A22; :: thesis: verum

for k being Nat st k >= n holds

x in A . k ; :: thesis: verum

( x in @lim_inf A iff x in lim_inf A )

proof

hence
lim_inf A = @lim_inf A
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in @lim_inf A iff x in lim_inf A )

then ex n being Nat st

for k being Nat holds x in A . (n + k) by SETLIM_1:67;

then ex n being Nat st

for k being Nat st k >= n holds

x in A . k by A19;

hence x in @lim_inf A by Th14; :: thesis: verum

end;hereby :: thesis: ( x in lim_inf A implies x in @lim_inf A )

assume
x in lim_inf A
; :: thesis: x in @lim_inf Aassume
x in @lim_inf A
; :: thesis: x in lim_inf A

then ex n being Nat st

for k being Nat st k >= n holds

x in A . k by Th14;

then ex n being Nat st

for k being Nat holds x in A . (n + k) by A19;

hence x in lim_inf A by SETLIM_1:67; :: thesis: verum

end;then ex n being Nat st

for k being Nat st k >= n holds

x in A . k by Th14;

then ex n being Nat st

for k being Nat holds x in A . (n + k) by A19;

hence x in lim_inf A by SETLIM_1:67; :: thesis: verum

then ex n being Nat st

for k being Nat holds x in A . (n + k) by SETLIM_1:67;

then ex n being Nat st

for k being Nat st k >= n holds

x in A . k by A19;

hence x in @lim_inf A by Th14; :: thesis: verum

proof

(Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1
reconsider CA = Complement A as SetSequence of Sigma ;

for x being object holds

( x in @lim_inf (Complement A) iff x in (@lim_sup A) ` )

end;for x being object holds

( x in @lim_inf (Complement A) iff x in (@lim_sup A) ` )

proof

hence
@lim_inf (Complement A) = (@lim_sup A) `
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in @lim_inf (Complement A) iff x in (@lim_sup A) ` )

x in Omega \ (@lim_sup A) by A24, SUBSET_1:def 4;

then not x in @Intersection (Union_Shift_Seq A) by XBOOLE_0:def 5;

then ex m being Nat st

for n being Nat st n >= m holds

not x in A . n by Th14;

then x in @lim_inf CA by A24, Th14;

hence x in @lim_inf (Complement A) ; :: thesis: verum

end;hereby :: thesis: ( x in (@lim_sup A) ` implies x in @lim_inf (Complement A) )

assume A24:
x in (@lim_sup A) `
; :: thesis: x in @lim_inf (Complement A)assume
x in @lim_inf (Complement A)
; :: thesis: x in (@lim_sup A) `

then x in @lim_inf CA ;

then ( x in Omega & ex n being Nat st

for k being Nat st k >= n holds

not x in A . k ) by Th14;

then ( x in Omega & not x in @lim_sup A ) by Th14;

then x in Omega \ (@lim_sup A) by XBOOLE_0:def 5;

hence x in (@lim_sup A) ` by SUBSET_1:def 4; :: thesis: verum

end;then x in @lim_inf CA ;

then ( x in Omega & ex n being Nat st

for k being Nat st k >= n holds

not x in A . k ) by Th14;

then ( x in Omega & not x in @lim_sup A ) by Th14;

then x in Omega \ (@lim_sup A) by XBOOLE_0:def 5;

hence x in (@lim_sup A) ` by SUBSET_1:def 4; :: thesis: verum

x in Omega \ (@lim_sup A) by A24, SUBSET_1:def 4;

then not x in @Intersection (Union_Shift_Seq A) by XBOOLE_0:def 5;

then ex m being Nat st

for n being Nat st n >= m holds

not x in A . n by Th14;

then x in @lim_inf CA by A24, Th14;

hence x in @lim_inf (Complement A) ; :: thesis: verum

proof

hence
( lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )
by A1, A18, A23; :: thesis: verum
(Prob . (([#] Sigma) \ (@lim_sup A))) + (Prob . (@lim_sup A)) = 1
by PROB_1:31;

hence (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 by A23, SUBSET_1:def 4; :: thesis: verum

end;hence (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 by A23, SUBSET_1:def 4; :: thesis: verum