theorem Th58: :: RLTOPSP1:58

for X being LinearTopSpace
for B being local_base of X
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )