let T be non empty TopSpace; :: thesis: for R, S being SetSequence of the carrier of T st R is subsequence of S holds
Lim_inf S c= Lim_inf R
let R, S be SetSequence of the carrier of T; :: thesis: ( R is subsequence of S implies Lim_inf S c= Lim_inf R )
assume R is subsequence of S ; :: thesis: Lim_inf S c= Lim_inf R
then consider Nseq being increasing sequence of NAT such that
A1: R = S * Nseq by VALUED_0:def 17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_inf S or x in Lim_inf R )
assume A2: x in Lim_inf S ; :: thesis: x in Lim_inf R
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
R . 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
R . m meets G
consider k being Nat such that
A3: for m being Nat st m > k holds
S . m meets G by A2, Def1;
take k ; :: thesis: for m being Nat st m > k holds
R . m meets G
let m1 be Nat; :: thesis: ( m1 > k implies R . m1 meets G )
A4: m1 in NAT by ORDINAL1:def 12;
A5: m1 <= Nseq . m1 by SEQM_3:14;
assume m1 > k ; :: thesis: R . m1 meets G
then A6: Nseq . m1 > k by A5, XXREAL_0:2;
dom Nseq = NAT by FUNCT_2:def 1;
then R . m1 = S . (Nseq . m1) by A1, FUNCT_1:13, A4;
hence R . m1 meets G by A3, A6; :: thesis: verum

end;

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