apply Iff.intro
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a ↔ a ∈ s
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s

case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a