no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s : Set α
B : Set (Set α)
hB : IsTopologicalBasis B
a : α
⊢ HasBasis (𝓝 a) (fun s => a ∈ s ∧ s ∈ B) closure
simpa only [and_comm] using hB.nhds_hasBasis.nhds_closure