[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace γ
a b c : α
h : a ≤ b
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
⊢ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) = s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace γ
a b c : α
h : a ≤ b
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
x✝ : { x // x ∈ Icc a b }
⊢ x✝ ∈ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) ↔ x✝ ∈ s
[PROOFSTEP]
simp
