theorem :: FINTOPO7:18

for ET being FMT_TopSpace
for cF being Filter of the carrier of ET
for cS being non empty Subset of cF
for A being non empty Subset of ET st cF = Neighborhood A & cS = OpenNeighborhoods A holds
cS is filter_basis