theorem Th10: :: CARDFIL3:29

for X being LinearTopSpace
for x being Point of X
for O being local_base of X
for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds
B is basis of (BOOL2F (NeighborhoodSystem x))