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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup C or x in (lim_sup A) \/ (lim_sup B) )
assume A2: x in lim_sup C ; :: thesis: x in (lim_sup A) \/ (lim_sup B)
( 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: for n being Nat ex k being Nat st x in B . (n + k)
given n2 being Nat such that A4: for k being Nat holds not x in B . (n2 + k) ; :: thesis: contradiction
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 ( x in A . (n + k) or x in B . (n + k) ) by A8, XBOOLE_0:def 3;

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

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

end;

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

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

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: verum

end;

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

proof

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

per cases ( x in lim_sup A or x in lim_sup B ) by A9, XBOOLE_0:def 3;

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

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

proof

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

end;

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

end;

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

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

proof

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

end;

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

end;

end;

end;