:: deftheorem defines Neighborhood FINTOPO7:def 7 :
for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being Subset of ET holds Neighborhood A = { N where N is a_neighborhood of A : verum } ;