let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let Prob be Probability of Sigma; :: thesis:
let A be SetSequence of Sigma; :: thesis:
thus A1: lim_sup A = @lim_sup A :: thesis:

A2: for n being Element of NAT
for x being set holds
( ex k being Element of NAT st x in (A ^\ n) . k iff ex k being Element of NAT st
( k >= n & x in A . k ) )

let n be Element of NAT ; :: thesis:
let x be set ; :: thesis:

hereby :: thesis:

assume ex k being Element of NAT st x in (A ^\ n) . k ; :: thesis:
then consider k being Element of NAT such that
A3: x in (A ^\ n) . k ;
A4: x in A . (k + n) by A3, NAT_1:def 3;
consider k being Element of NAT such that
A5: x in A . (k + n) by A4;
consider k being Element of NAT such that
A6: ( k >= n & x in A . k ) by A5, NAT_1:11;
thus ex k being Element of NAT st
( k >= n & x in A . k ) by A6; :: thesis:

end;

assume ex k being Element of NAT st
( k >= n & x in A . k ) ; :: thesis:
then consider k being Element of 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 Element of NAT by ORDINAL1:def 12;
A9: ( x in A . k implies x in (A ^\ n) . knat ) by A8, NAT_1:def 3;
thus ex k being Element of NAT st x in (A ^\ n) . k by A7, A9; :: thesis:

end;

A10: for x being set holds
( ( for m being Element of NAT ex n being Element of NAT st
( n >= m & x in A . n ) ) iff for m being Element of NAT ex n being Element of NAT st x in A . (m + n) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A11: for m being Element of NAT ex n being Element of NAT st
( n >= m & x in A . n ) ; :: thesis:
thus for m being Element of NAT ex n being Element of NAT st x in A . (m + n) :: thesis:

proof

let m be Element of NAT ; :: thesis:
ex n being Element of NAT st
( n >= m & x in A . n ) by A11;
then consider n being Element of NAT such that
A12: x in (A ^\ m) . n by A2;
x in A . (m + n) by A12, NAT_1:def 3;
hence ex n being Element of NAT st x in A . (m + n) ; :: thesis:

end;

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

proof

let m be Element of NAT ; :: thesis:
consider n being Element of NAT such that
A14: x in A . (m + n) by A13;
x in (A ^\ m) . n by A14, NAT_1:def 3;
hence ex n being Element of NAT st
( n >= m & x in A . n ) by A2; :: thesis:

end;

A15: for x being set holds
( x in @Intersection (Union_Shift_Seq A) iff for m being Element of NAT ex n being Element of NAT st x in A . (m + n) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in @Intersection (Union_Shift_Seq A) ; :: thesis:
then A16: for m being Element of NAT ex n being Element of NAT st
( n >= m & x in A . n ) by Th14;
thus for m being Element of NAT ex n being Element of NAT st x in A . (m + n) by A16, A10; :: thesis:

end;

assume for m being Element of NAT ex n being Element of NAT st x in A . (m + n) ; :: thesis:
then for m being Element of NAT ex n being Element of NAT st
( n >= m & x in A . n ) by A10;
hence x in @Intersection (Union_Shift_Seq A) by Th14; :: thesis:

end;

for x being set holds
( x in lim_sup A iff x in @Intersection (Union_Shift_Seq A) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in lim_sup A ; :: thesis:
then A17: for m being Element of NAT ex n being Element of NAT st x in A . (m + n) by SETLIM_1:66;
thus x in @Intersection (Union_Shift_Seq A) by A17, A15; :: thesis:

end;

assume x in @Intersection (Union_Shift_Seq A) ; :: thesis:
then for m being Element of NAT ex n being Element of NAT st x in A . (m + n) by A15;
hence x in lim_sup A by SETLIM_1:66; :: thesis:

end;

hence lim_sup A = @lim_sup A by TARSKI:1; :: thesis:

end;

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

proof

let A be SetSequence of Sigma; :: thesis:
A19: for x being set holds
( ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k iff ex n being Element of NAT st
for k being Element of NAT holds x in A . (n + k) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k ; :: thesis:
then consider n being Element of NAT such that
A20: for k being Element of NAT st k >= n holds
x in A . k ;
for k being Element of NAT holds x in A . (n + k) by A20, NAT_1:11;
hence ex n being Element of NAT st
for k being Element of NAT holds x in A . (n + k) ; :: thesis:

end;

assume ex n being Element of NAT st
for k being Element of NAT holds x in A . (n + k) ; :: thesis:
then consider n being Element of NAT such that
A21: for k being Element of NAT holds x in A . (n + k) ;
for k being Element of NAT st k >= n holds
x in A . k

proof

let k be Element of NAT ; :: thesis:
assume n <= k ; :: thesis:
then consider knat being Nat such that
A22: k = n + knat by NAT_1:10;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
x in A . (n + knat) by A21;
hence x in A . k by A22; :: thesis:

end;

hence ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k ; :: thesis:

end;

for x being set holds
( x in @lim_inf A iff x in lim_inf A )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in @lim_inf A ; :: thesis:
then ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k by Th14;
then ex n being Element of NAT st
for k being Element of NAT holds x in A . (n + k) by A19;
hence x in lim_inf A by SETLIM_1:67; :: thesis:

end;

assume x in lim_inf A ; :: thesis:
then ex n being Element of NAT st
for k being Element of NAT holds x in A . (n + k) by SETLIM_1:67;
then ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k by A19;
hence x in @lim_inf A by Th14; :: thesis:

end;

hence lim_inf A = @lim_inf A by TARSKI:1; :: thesis:

end;

A23: @lim_inf (Complement A) = (@lim_sup A) `

proof

reconsider CA = Complement A as SetSequence of Sigma ;
for x being set holds
( x in @lim_inf (Complement A) iff x in (@lim_sup A) ` )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in @lim_inf (Complement A) ; :: thesis:
then x in @lim_inf CA ;
then ( x in Omega & ex n being Element of NAT st
for k being Element of 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:

end;

assume A24: x in (@lim_sup A) ` ; :: thesis:
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 Element of NAT st
for n being Element of 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:

end;

hence @lim_inf (Complement A) = (@lim_sup A) ` by TARSKI:1; :: thesis:

end;

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

proof

(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:

end;

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: