theorem Th30: :: C0SP3:30

for X being NormedLinearTopSpace
for V being Subset of X
for x being Point of X holds
( V is a_neighborhood of x iff ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) )