for T being non empty TopSpace
for R, S being SetSequence of the carrier of T st R is subsequence of S holds
Lim_inf S c= Lim_inf R