theorem Th40: :: CARDFIL2:90

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
( B is_coarser_than s .: base_of_frechet_filter iff for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b )