theorem Th59: :: RLTOPSP1:59

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