for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being Subset of ET
for NA being a_neighborhood of A
for B being Subset of ET st NA c= B holds
B is a_neighborhood of A