let X be set ; :: thesis: for A, B being SetSequence of X
for C being Subset of X st ( for n being Element of 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 Element of 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 Element of NAT holds B . n = C \+\ (A . n) ) implies C \+\ (lim_sup A) c= lim_sup B )
assume A1: for n being Element of NAT holds B . n = C \+\ (A . n) ; :: thesis: C \+\ (lim_sup A) c= lim_sup B
let x be set ; :: 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 Element of NAT such that
A4: for k being Element of NAT holds not x in A . (n + k) by Th8;
for m being Element of NAT ex k being Element of NAT st x in B . (m + k)

proof

let m be Element of NAT ; :: thesis: ex k being Element of 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 Th8; :: thesis: verum

end;

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

for m being Element of NAT ex k being Element of NAT st x in B . (m + k)

proof

let m be Element of NAT ; :: thesis: ex k being Element of NAT st x in B . (m + k)
consider k being Element of NAT such that
A6: x in A . (m + k) by A5, Th8;
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 Th8; :: thesis: verum

end;

end;