for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b )