for S being SetSequence of the carrier of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is compact by Th25, TOPREAL6:79;