let T be non empty TopSpace; :: thesis:
let A, B, C be SetSequence of the carrier of T; :: thesis:
assume A1: for i being Nat holds C . i = (A . i) /\ (B . i) ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in Lim_inf C ; :: thesis:
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:
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:
let m be Nat; :: thesis:
assume m > k ; :: thesis:
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:

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:
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:
let m be Nat; :: thesis:
assume m > k ; :: thesis:
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:

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: