theorem :: RLTOPSP1:45

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