:: deftheorem Def1 defines Neighbourhood NFCONT_1:def 1 :
for S being RealNormSpace
for x0 being Point of S
for b₃ being Subset of S holds
( b₃ is Neighbourhood of x0 iff ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b₃ ) );