let X be set ; :: thesis:
let A, B, C be SetSequence of X; :: thesis:
assume A1: for n being Nat holds C . n = (A . n) \/ (B . n) ; :: thesis:
thus lim_sup C c= (lim_sup A) \/ (lim_sup B) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in lim_sup C ; :: thesis:
( for n being Nat ex k being Nat st x in A . (n + k) or for n being Nat ex k being Nat st x in B . (n + k) )

proof

given n1 being Nat such that A3: for k being Nat holds not x in A . (n1 + k) ; :: thesis:
given n2 being Nat such that A4: for k being Nat holds not x in B . (n2 + k) ; :: thesis:
set n = max (n1,n2);
consider g being Nat such that
A5: max (n1,n2) = n1 + g by NAT_1:10, XXREAL_0:25;
consider h being Nat such that
A6: max (n1,n2) = n2 + h by NAT_1:10, XXREAL_0:25;
reconsider n = max (n1,n2) as Nat by TARSKI:1;
consider k being Nat such that
A7: x in C . (n + k) by A2, Th5;
A8: x in (A . (n + k)) \/ (B . (n + k)) by A1, A7;

per cases by A8, XBOOLE_0:def 3;

suppose x in A . (n + k) ; :: thesis:

then x in A . (n1 + (g + k)) by A5;
hence contradiction by A3; :: thesis:

end;

suppose x in B . (n + k) ; :: thesis:

then x in B . (n2 + (h + k)) by A6;
hence contradiction by A4; :: thesis:

end;

end;

end;

then ( x in lim_sup A or x in lim_sup B ) by Th5;
hence x in (lim_sup A) \/ (lim_sup B) by XBOOLE_0:def 3; :: thesis:

end;

thus (lim_sup A) \/ (lim_sup B) c= lim_sup C :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: x in (lim_sup A) \/ (lim_sup B) ; :: thesis:

per cases by A9, XBOOLE_0:def 3;

suppose A10: x in lim_sup A ; :: thesis:

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

proof

let n be Nat; :: thesis:
consider k being Nat such that
A11: x in A . (n + k) by A10, Th5;
take k ; :: thesis:
x in (A . (n + k)) \/ (B . (n + k)) by A11, XBOOLE_0:def 3;
hence x in C . (n + k) by A1; :: thesis:

end;

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

end;

suppose A12: x in lim_sup B ; :: thesis:

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

proof

let n be Nat; :: thesis:
consider k being Nat such that
A13: x in B . (n + k) by A12, Th5;
take k ; :: thesis:
x in (A . (n + k)) \/ (B . (n + k)) by A13, XBOOLE_0:def 3;
hence x in C . (n + k) by A1; :: thesis:

end;

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

end;

end;

end;