theorem :: CARDFIL3:28

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