theorem :: CARDFIL3:26

for X being LinearTopSpace holds NeighborhoodSystem (0. X) is local_base of X