let T be non empty TopSpace; :: thesis: for x being Point of T holds NeighborhoodSystem x is filter_base of ([#] T)
let x be Point of T; :: thesis: NeighborhoodSystem x is filter_base of ([#] T)
reconsider Nx = NeighborhoodSystem x as Filter of [#] T by Th36;
Nx is basis of Nx by Th03;
hence NeighborhoodSystem x is filter_base of ([#] T) by Th09; :: thesis: verum