let A, B, C be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) implies (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C )
assume A1: for i being Element of NAT holds C . i = (A . i) \/ (B . i) ; :: thesis: (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C
A2: for i being Element of NAT holds A . i c= C . i

proof

let i be Element of NAT ; :: thesis: A . i c= C . i
C . i = (A . i) \/ (B . i) by A1;
hence A . i c= C . i by XBOOLE_1:7; :: thesis: verum

end;

A3: for i being Element of NAT holds B . i c= C . i

proof

let i be Element of NAT ; :: thesis: B . i c= C . i
C . i = (A . i) \/ (B . i) by A1;
hence B . i c= C . i by XBOOLE_1:7; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Lim_sup A) \/ (Lim_sup B) or x in Lim_sup C )
assume A4: 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 A4, XBOOLE_0:def 3;

suppose x in Lim_sup A ; :: thesis: x in Lim_sup C

then consider A1 being subsequence of A such that
A5: x in Lim_inf A1 by Def12;
consider C1 being subsequence of C such that
A6: for i being Element of NAT holds A1 . i c= C1 . i by A2, Th69;
Lim_inf A1 c= Lim_inf C1 by A6, Th54;
hence x in Lim_sup C by A5, Def12; :: thesis: verum

end;

suppose x in Lim_sup B ; :: thesis: x in Lim_sup C

then consider B1 being subsequence of B such that
A7: x in Lim_inf B1 by Def12;
consider C1 being subsequence of C such that
A8: for i being Element of NAT holds B1 . i c= C1 . i by A3, Th69;
Lim_inf B1 c= Lim_inf C1 by A8, Th54;
hence x in Lim_sup C by A7, Def12; :: thesis: verum

end;

end;

end;