theorem :: CARDFIL3:27

for X being LinearTopSpace
for O being local_base of X
for a being Point of X
for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds
P is basis of a