for X being LinearTopSpace
for P being Subset-Family of X st P = { U where U is a_neighborhood of 0. X : verum } holds
P is local_base of X