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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in lim_inf F ; :: thesis:
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)

let k be Nat; :: thesis:
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:
then not x in F . (n + k) by A3, XBOOLE_0:def 5;
hence contradiction by A2; :: thesis:

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:

end;

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in (lim_sup (Complement F)) ` ; :: thesis:
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)

let k be Nat; :: thesis:
reconsider nk = n + k as Element of NAT by ORDINAL1:def 12;
assume not x in F . (n + k) ; :: thesis:
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:

end;

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

end;