for M being non empty MetrSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of (TopSpaceMetr M)
for x being Point of (TopSpaceMetr M)
for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ) by CARDFIL2:84;