:: deftheorem Def6 defines a_neighborhood FINTOPO7:def 6 :
for ET being non empty strict U_FMT_filter FMT_Space_Str
for A, b₃ being Subset of ET holds
( b₃ is a_neighborhood of A iff for x being Element of ET st x in A holds
b₃ in U_FMT x );