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 C c= (Lim_inf A) /\ (Lim_inf B)
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 C c= (Lim_inf A) /\ (Lim_inf B) )
assume A1: for i being Nat holds C . i = (A . i) /\ (B . i) ; :: thesis: Lim_inf C c= (Lim_inf A) /\ (Lim_inf B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_inf C or x in (Lim_inf A) /\ (Lim_inf B) )
assume A2: x in Lim_inf C ; :: thesis: x in (Lim_inf A) /\ (Lim_inf B)
then reconsider p = x as Point of T ;
for H being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
B . 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
B . m meets H
consider k being Nat such that
A3: for m being Nat st m > k holds
C . m meets H by A2, Def1;
take k ; :: thesis: for m being Nat st m > k holds
B . m meets H
let m be Nat; :: thesis: ( m > k implies B . m meets H )
assume m > k ; :: thesis: B . m meets H
then A4: C . m meets H by A3;
C . m = (A . m) /\ (B . m) by A1;
hence B . m meets H by A4, XBOOLE_1:17, XBOOLE_1:63; :: thesis: verum

end;

then A5: x in Lim_inf B by Def1;
for H being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
A . 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
A . m meets H
consider k being Nat such that
A6: for m being Nat st m > k holds
C . m meets H by A2, Def1;
take k ; :: thesis: for m being Nat st m > k holds
A . m meets H
let m be Nat; :: thesis: ( m > k implies A . m meets H )
assume m > k ; :: thesis: A . m meets H
then A7: C . m meets H by A6;
C . m = (A . m) /\ (B . m) by A1;
hence A . m meets H by A7, XBOOLE_1:17, XBOOLE_1:63; :: thesis: verum

end;

then x in Lim_inf A by Def1;
hence x in (Lim_inf A) /\ (Lim_inf B) by A5, XBOOLE_0:def 4; :: thesis: verum