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 () = () ` & (Prob . ()) + (Prob . ()) = 1 & (Prob . ()) + (Prob . ()) = 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 () = () ` & (Prob . ()) + (Prob . ()) = 1 & (Prob . ()) + (Prob . ()) = 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 () = () ` & (Prob . ()) + (Prob . ()) = 1 & (Prob . ()) + (Prob . ()) = 1 )

let A be SetSequence of Sigma; :: thesis: ( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf () = () ` & (Prob . ()) + (Prob . ()) = 1 & (Prob . ()) + (Prob . ()) = 1 )
thus A1: lim_sup A = @lim_sup A :: thesis: ( lim_inf A = @lim_inf A & @lim_inf () = () ` & (Prob . ()) + (Prob . ()) = 1 & (Prob . ()) + (Prob . ()) = 1 )
proof
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 ) )
proof
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 ) )

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 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 ;
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 ;
thus ex k being Nat st
( k >= n & x in A . k ) by A6; :: thesis: verum
end;
assume ex k being Nat st
( 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 ;
reconsider knat = knat as Nat ;
A9: ( x in A . k implies x in (A ^\ n) . knat ) by ;
thus ex k being Nat st x in (A ^\ n) . k by A7, A9; :: thesis: verum
end;
A10: for x being object holds
( ( 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
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) )

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 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
proof
let m be Nat; :: thesis: ex n being Nat st x in A . (m + n)
ex n being Nat st
( n >= m & x in A . n ) by A11;
then consider n being Nat such that
A12: x in (A ^\ m) . n by A2;
x in A . (m + n) by ;
hence ex n being Nat st x in A . (m + n) ; :: thesis: verum
end;
end;
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 )

thus for m being Nat ex n being Nat st
( n >= m & x in A . n ) :: thesis: verum
proof
let m be Nat; :: thesis: ex n being Nat st
( n >= m & x in A . n )

consider n being Nat such that
A14: x in A . (m + n) by A13;
x in (A ^\ m) . n by ;
hence ex n being Nat st
( n >= m & x in A . n ) by A2; :: thesis: verum
end;
end;
A15: for x being object holds
( x in @Intersection () iff for m being Nat ex n being Nat st x in A . (m + n) )
proof
let x be object ; :: thesis: ( x in @Intersection () 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 x in @Intersection () )
assume x in @Intersection () ; :: 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 ; :: thesis: verum
end;
assume for m being Nat ex n being Nat st x in A . (m + n) ; :: thesis:
then for m being Nat ex n being Nat st
( n >= m & x in A . n ) by A10;
hence x in @Intersection () by Th14; :: thesis: verum
end;
for x being object holds
( x in lim_sup A iff x in @Intersection () )
proof
let x be object ; :: thesis: ( x in lim_sup A iff x in @Intersection () )
hereby :: thesis: ( x in @Intersection () implies x in lim_sup A )
assume x in lim_sup A ; :: thesis:
then A17: for m being Nat ex n being Nat st x in A . (m + n) by SETLIM_1:66;
thus x in @Intersection () by ; :: thesis: verum
end;
assume x in @Intersection () ; :: thesis:
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;
hence lim_sup A = @lim_sup A by TARSKI:2; :: thesis: verum
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 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
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) )

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 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 ;
hence ex n being Nat st
for k being Nat holds x in A . (n + k) ; :: thesis: verum
end;
assume ex n being Nat st
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
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;
hence ex n being Nat st
for k being Nat st k >= n holds
x in A . k ; :: thesis: verum
end;
for x being object holds
( x in @lim_inf A iff x in lim_inf A )
proof
let x be object ; :: thesis: ( x in @lim_inf A iff x in lim_inf A )
hereby :: thesis: ( x in lim_inf A implies x in @lim_inf A )
assume x in @lim_inf A ; :: thesis:
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;
assume x in lim_inf A ; :: thesis:
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;
hence lim_inf A = @lim_inf A by TARSKI:2; :: thesis: verum
end;
A23: @lim_inf () = () `
proof
reconsider CA = Complement A as SetSequence of Sigma ;
for x being object holds
( x in @lim_inf () iff x in () ` )
proof
let x be object ; :: thesis: ( x in @lim_inf () iff x in () ` )
hereby :: thesis: ( x in () ` implies x in @lim_inf () )
assume x in @lim_inf () ; :: thesis: x in () `
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 \ () by XBOOLE_0:def 5;
hence x in () ` by SUBSET_1:def 4; :: thesis: verum
end;
assume A24: x in () ` ; :: thesis: x in @lim_inf ()
x in Omega \ () by ;
then not x in @Intersection () 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 ;
hence x in @lim_inf () ; :: thesis: verum
end;
hence @lim_inf () = () ` by TARSKI:2; :: thesis: verum
end;
(Prob . ()) + (Prob . ()) = 1
proof
(Prob . (([#] Sigma) \ ())) + (Prob . ()) = 1 by PROB_1:31;
hence (Prob . ()) + (Prob . ()) = 1 by ; :: thesis: verum
end;
hence ( lim_inf A = @lim_inf A & @lim_inf () = () ` & (Prob . ()) + (Prob . ()) = 1 & (Prob . ()) + (Prob . ()) = 1 ) by A1, A18, A23; :: thesis: verum