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