for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S holds Lim S c= Lim S1