no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
P : Set α → Prop
hP : ∀ (s t : Set α), s ⊆ t → P s → P t
⊢ (∀ (i : Set α), x ∈ i ∧ IsOpen i → P i) ↔ ∀ (s : Set α), IsOpen s → x ∈ s → P s
simp only [@and_comm (x ∈ _), and_imp]