:: deftheorem Def6 defines Neighbourhood RCOMP_1:def 6 :
for r being Real
for b₂ being Subset of REAL holds
( b₂ is Neighbourhood of r iff ex g being Real st
( 0 < g & b₂ = ].(r - g),(r + g).[ ) );