theorem :: KURATO_2:21

for n being Nat
for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Nat holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S