no goals
α : Type u_1
β : Type ?u.397946
γ : Type ?u.397949
δ : Type ?u.397952
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'
simpa [hx] using ext_iff.1 ht x