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

end;

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