no goals
α : Type u_1
β : Type ?u.1151
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iic a] a ⊔ 𝓝[Ici a] a = 𝓝 a
rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]