let X be set ; :: thesis:
let A, B be SetSequence of X; :: thesis:
let C be Subset of X; :: thesis:
assume A1: for n being Nat holds B . n = C \+\ (A . n) ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in C \+\ (lim_inf A) ; :: thesis:

per cases by A2, XBOOLE_0:1;

suppose A3: ( x in C & not x in lim_inf A ) ; :: thesis:

for n being Nat ex k being Nat st x in B . (n + k)

proof

let n be Nat; :: thesis:
consider k being Nat such that
A4: not x in A . (n + k) by A3, Th4;
take k ; :: thesis:
x in C \+\ (A . (n + k)) by A3, A4, XBOOLE_0:1;
hence x in B . (n + k) by A1; :: thesis:

end;

hence x in lim_sup B by Th5; :: thesis:

end;

suppose A5: ( not x in C & x in lim_inf A ) ; :: thesis:

then consider n being Nat such that
A6: for k being Nat holds x in A . (n + k) by Th4;
for m being Nat ex k being Nat st x in B . (m + k)

proof

let m be Nat; :: thesis:
take k = n; :: thesis:
x in A . (m + k) by A6;
then x in C \+\ (A . (m + k)) by A5, XBOOLE_0:1;
hence x in B . (m + k) by A1; :: thesis:

end;

hence x in lim_sup B by Th5; :: thesis:

end;

end;