theorem Th51: :: CARDFIL4:60

for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B )