let n be Nat; :: thesis: for A, B being SetSequence of the carrier of (TOP-REAL n)
for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
let A, B be SetSequence of the carrier of (TOP-REAL n); :: thesis: for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
let C be SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: ( ( for i being Nat holds C . i = [:(A . i),(B . i):] ) implies [:(Lim_inf A),(Lim_inf B):] = Lim_inf C )
assume A1: for i being Nat holds C . i = [:(A . i),(B . i):] ; :: thesis: [:(Lim_inf A),(Lim_inf B):] = Lim_inf C
thus [:(Lim_inf A),(Lim_inf B):] c= Lim_inf C :: according to XBOOLE_0:def 10 :: thesis: Lim_inf C c= [:(Lim_inf A),(Lim_inf B):]

proof

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 consider x1, x2 being object such that
A3: x1 in Lim_inf A and
A4: x2 in Lim_inf B and
A5: x = [x1,x2] by ZFMISC_1:def 2;
reconsider p = x as Point of [:(TOP-REAL n),(TOP-REAL n):] by A2;
reconsider x1 = x1, x2 = x2 as Point of (TOP-REAL n) by A3, A4;
for G being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
C . m meets G

proof

let G be a_neighborhood of p; :: thesis: ex k being Nat st
for m being Nat st m > k holds
C . m meets G
G is a_neighborhood of [:{x1},{x2}:] by A5, Th11;
then consider V being a_neighborhood of {x1}, W being a_neighborhood of x2 such that
A6: [:V,W:] c= G by BORSUK_1:25;
consider k2 being Nat such that
A7: for m being Nat st m > k2 holds
B . m meets W by A4, Def1;
V is a_neighborhood of x1 by CONNSP_2:8;
then consider k1 being Nat such that
A8: for m being Nat st m > k1 holds
A . m meets V by A3, Def1;
reconsider k = max (k1,k2) as Nat by TARSKI:1;
take k ; :: thesis: for m being Nat st m > k holds
C . m meets G
let m be Nat; :: thesis: ( m > k implies C . m meets G )
assume A9: m > k ; :: thesis: C . m meets G
k >= k2 by XXREAL_0:25;
then m > k2 by A9, XXREAL_0:2;
then A10: B . m meets W by A7;
k >= k1 by XXREAL_0:25;
then m > k1 by A9, XXREAL_0:2;
then A . m meets V by A8;
then [:(A . m),(B . m):] meets [:V,W:] by A10, KURATO_0:2;
then C . m meets [:V,W:] by A1;
hence C . m meets G by A6, XBOOLE_1:63; :: thesis: verum

end;

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

end;

thus Lim_inf C c= [:(Lim_inf A),(Lim_inf B):] :: thesis: verum

proof

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 A11: x in Lim_inf C ; :: thesis: x in [:(Lim_inf A),(Lim_inf B):]
then x in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then A12: x in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def 2;
then reconsider p1 = x `1 , p2 = x `2 as Point of (TOP-REAL n) by MCART_1:10;
set H = the a_neighborhood of p2;
set F = the a_neighborhood of p1;
A13: x = [p1,p2] by A12, MCART_1:21;
for G being a_neighborhood of p2 ex k being Nat st
for m being Nat st m > k holds
B . m meets G

proof

let G be a_neighborhood of p2; :: thesis: ex k being Nat st
for m being Nat st m > k holds
B . m meets G
consider k being Nat such that
A14: for m being Nat st m > k holds
C . m meets [: the a_neighborhood of p1,G:] by A11, A13, Def1;
take k ; :: thesis: for m being Nat st m > k holds
B . m meets G
let m be Nat; :: thesis: ( m > k implies B . m meets G )
assume m > k ; :: thesis: B . m meets G
then C . m meets [: the a_neighborhood of p1,G:] by A14;
then consider y being object such that
A15: y in C . m and
A16: y in [: the a_neighborhood of p1,G:] by XBOOLE_0:3;
y in [:(A . m),(B . m):] by A1, A15;
then A17: y `2 in B . m by MCART_1:10;
y `2 in G by A16, MCART_1:10;
hence B . m meets G by A17, XBOOLE_0:3; :: thesis: verum

end;

then A18: p2 in Lim_inf B by Def1;
for G being a_neighborhood of p1 ex k being Nat st
for m being Nat st m > k holds
A . m meets G

proof

let G be a_neighborhood of p1; :: thesis: ex k being Nat st
for m being Nat st m > k holds
A . m meets G
consider k being Nat such that
A19: for m being Nat st m > k holds
C . m meets [:G, the a_neighborhood of p2:] by A11, A13, Def1;
take k ; :: thesis: for m being Nat st m > k holds
A . m meets G
let m be Nat; :: thesis: ( m > k implies A . m meets G )
assume m > k ; :: thesis: A . m meets G
then C . m meets [:G, the a_neighborhood of p2:] by A19;
then consider y being object such that
A20: y in C . m and
A21: y in [:G, the a_neighborhood of p2:] by XBOOLE_0:3;
y in [:(A . m),(B . m):] by A1, A20;
then A22: y `1 in A . m by MCART_1:10;
y `1 in G by A21, MCART_1:10;
hence A . m meets G by A22, XBOOLE_0:3; :: thesis: verum

end;

then p1 in Lim_inf A by Def1;
hence x in [:(Lim_inf A),(Lim_inf B):] by A13, A18, ZFMISC_1:87; :: thesis: verum

end;