theorem Th39: :: CARDFIL2:89

for T being non empty TopSpace
for s being sequence of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) iff B is_coarser_than s .: base_of_frechet_filter )