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 set ; :: 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 Element of NAT such that
A2: for k being Element of NAT holds x in F . (n + k) by Th7;
for k being Element of NAT holds not x in (Complement F) . (n + k)

proof

let k be Element of NAT ; :: thesis: not x in (Complement F) . (n + k)
A3: (Complement F) . (n + k) = (F . (n + k)) ` 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 Th8;
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 set ; :: 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 Element of NAT such that
A5: for k being Element of NAT holds not x in (Complement F) . (n + k) by Th8;
for k being Element of NAT holds x in F . (n + k)

proof

let k be Element of NAT ; :: thesis: x in F . (n + k)
assume not x in F . (n + k) ; :: thesis: contradiction
then x in (F . (n + k)) ` 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 Th7; :: thesis: verum

end;