let A, B, C be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds C . i = (A . i) \/ (B . i) ) implies (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C )
assume A1: for i being Nat holds C . i = (A . i) \/ (B . i) ; :: thesis: (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C
A2: for i being Nat holds B . i c= C . i
proof
let i be 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;
A3: for i being Nat holds A . i c= C . i
proof
let i be 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;
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 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 Def2;
consider C1 being subsequence of C such that
A6: for i being Nat holds A1 . i c= C1 . i by A3, Th32;
Lim_inf A1 c= Lim_inf C1 by A6, Th17;
hence x in Lim_sup C by A5, Def2; :: 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 Def2;
consider C1 being subsequence of C such that
A8: for i being Nat holds B1 . i c= C1 . i by A2, Th32;
Lim_inf B1 c= Lim_inf C1 by A8, Th17;
hence x in Lim_sup C by A7, Def2; :: thesis: verum
end;
end;
end;