for X being LinearTopSpace
for U being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W is circled & W c= U )