for X being LinearTopSpace
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st Cl W c= V