no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.47710
G : Type ?u.47713
ι : Type ?u.47716
π : ι → Type ?u.47721
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ∈ s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s ↔ [x-[𝕜]y] ⊆ s
simp only [← insert_endpoints_openSegment, insert_subset, *, true_and_iff]