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

per cases ( ( x in C & not x in lim_inf A ) or ( not x in C & x in lim_inf A ) ) by A2, XBOOLE_0:1;

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

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

proof

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

end;

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

end;

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

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: ex k being Nat st x in B . (m + k)
take k = n; :: thesis: x in B . (m + k)
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: verum

end;

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

end;

end;