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