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_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_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_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_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 )
A18: for A being SetSequence of Sigma holds lim_inf A = @lim_inf A ;
A23: @lim_inf (Complement A) = (@lim_sup A) `

proof

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) ` )

proof

let x be object ; :: thesis: ( x in @lim_inf (Complement A) iff x in (@lim_sup A) ` )

hereby :: thesis: ( x in (@lim_sup A) ` implies 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;

assume A24: x in (@lim_sup A) ` ; :: thesis: x in @lim_inf (Complement A)
x in Omega \ (@lim_sup A) by A24, SUBSET_1:def 4;
then not x in Intersection (superior_setsequence 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;

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

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

end;

hence ( @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 A18, A23; :: thesis: verum