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 Element of NAT st
for j being Element of NAT st i <= j holds
s . j in b )