theorem :: CARDFIL3:32

for T being LinearTopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
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;