let X be set ; :: thesis: for F being SetSequence of X holds lim_inf F = (lim_sup (Complement F)) `
let F be SetSequence of X; :: thesis: lim_inf F = (lim_sup (Complement F)) `
set G = Complement F;
thus lim_inf F c= (lim_sup (Complement F)) ` :: according to XBOOLE_0:def 10 :: thesis: (lim_sup (Complement F)) ` c= lim_inf F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf F or x in (lim_sup (Complement F)) ` )
assume A1: x in lim_inf F ; :: thesis: x in (lim_sup (Complement F)) `
then consider n being Nat such that
A2: for k being Nat holds x in F . (n + k) by Th4;
for k being Nat holds not x in (Complement F) . (n + k)

proof

let k be Nat; :: thesis: not x in (Complement F) . (n + k)
reconsider nk = n + k as Element of NAT by ORDINAL1:def 12;
A3: (Complement F) . (n + k) = (F . nk) ` by PROB_1:def 2;
assume x in (Complement F) . (n + k) ; :: thesis: contradiction
then not x in F . (n + k) by A3, XBOOLE_0:def 5;
hence contradiction by A2; :: thesis: verum

end;

then not x in lim_sup (Complement F) by Th5;
hence x in (lim_sup (Complement F)) ` by A1, XBOOLE_0:def 5; :: thesis: verum

end;

thus (lim_sup (Complement F)) ` c= lim_inf F :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_sup (Complement F)) ` or x in lim_inf F )
assume A4: x in (lim_sup (Complement F)) ` ; :: thesis: x in lim_inf F
then not x in lim_sup (Complement F) by XBOOLE_0:def 5;
then consider n being Nat such that
A5: for k being Nat holds not x in (Complement F) . (n + k) by Th5;
for k being Nat holds x in F . (n + k)

proof

let k be Nat; :: thesis: x in F . (n + k)
reconsider nk = n + k as Element of NAT by ORDINAL1:def 12;
assume not x in F . (n + k) ; :: thesis: contradiction
then x in (F . nk) ` by A4, XBOOLE_0:def 5;
then x in (Complement F) . (n + k) by PROB_1:def 2;
hence contradiction by A5; :: thesis: verum

end;

hence x in lim_inf F by Th4; :: thesis: verum

end;