let T be non empty TopSpace; :: thesis: for A, B, C being SetSequence of the carrier of T st ( for i being Nat holds C . i = (A . i) \/ (B . i) ) holds
(Lim_inf A) \/ (Lim_inf B) c= Lim_inf C
let A, B, C be SetSequence of the carrier of T; :: thesis: ( ( for i being Nat holds C . i = (A . i) \/ (B . i) ) implies (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C )
assume A1: for i being Nat holds C . i = (A . i) \/ (B . i) ; :: thesis: (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Lim_inf A) \/ (Lim_inf B) or x in Lim_inf C )
assume A2: x in (Lim_inf A) \/ (Lim_inf B) ; :: thesis: x in Lim_inf C
then reconsider p = x as Point of T ;

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

suppose A3: x in Lim_inf A ; :: thesis: x in Lim_inf C

for H being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
C . m meets H

proof

let H be a_neighborhood of p; :: thesis: ex k being Nat st
for m being Nat st m > k holds
C . m meets H
consider k being Nat such that
A4: for m being Nat st m > k holds
A . m meets H by A3, Def1;
take k ; :: thesis: for m being Nat st m > k holds
C . m meets H
let m be Nat; :: thesis: ( m > k implies C . m meets H )
assume m > k ; :: thesis: C . m meets H
then A5: A . m meets H by A4;
C . m = (A . m) \/ (B . m) by A1;
hence C . m meets H by A5, XBOOLE_1:7, XBOOLE_1:63; :: thesis: verum

end;

hence x in Lim_inf C by Def1; :: thesis: verum

end;

suppose A6: x in Lim_inf B ; :: thesis: x in Lim_inf C

for H being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
C . m meets H

proof

let H be a_neighborhood of p; :: thesis: ex k being Nat st
for m being Nat st m > k holds
C . m meets H
consider k being Nat such that
A7: for m being Nat st m > k holds
B . m meets H by A6, Def1;
take k ; :: thesis: for m being Nat st m > k holds
C . m meets H
let m be Nat; :: thesis: ( m > k implies C . m meets H )
assume m > k ; :: thesis: C . m meets H
then A8: B . m meets H by A7;
C . m = (A . m) \/ (B . m) by A1;
hence C . m meets H by A8, XBOOLE_1:7, XBOOLE_1:63; :: thesis: verum

end;

hence x in Lim_inf C by Def1; :: thesis: verum

end;

end;