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_sup 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_sup 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_sup A) c= lim_sup B )
assume A1: for n being Nat holds B . n = C \+\ (A . n) ; :: thesis: C \+\ (lim_sup A) c= lim_sup B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C \+\ (lim_sup A) or x in lim_sup B )
assume A2: x in C \+\ (lim_sup A) ; :: thesis: x in lim_sup B

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

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

then consider n being Nat such that
A4: for k being Nat holds not x in A . (n + k) by Th5;
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)
not x in A . (m + k) by A4;
then x in C \+\ (A . (m + k)) by A3, 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;

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

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)
consider k being Nat such that
A6: x in A . (m + k) by A5, Th5;
take k ; :: thesis: x in B . (m + k)
x in C \+\ (A . (m + k)) by A5, A6, 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;