theorem Th25: :: KURATO_2:25

for n being Nat
for S being SetSequence of the carrier of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is bounded