for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET