theorem :: FINTOPO7:17

for ET being FMT_TopSpace
for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET by Th7bis;