𝕜 : Type u_2
E : Type u_1
F : Type ?u.46146
G : Type ?u.46149
ι : Type ?u.46152
π : ι → Type ?u.46157
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.46146
G : Type ?u.46149
ι : Type ?u.46152
π : ι → Type ?u.46157
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ [x-[𝕜]y]
⊢ z ∈ openSegment 𝕜 x y
rw [← insert_endpoints_openSegment] at hz
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.46146
G : Type ?u.46149
ι : Type ?u.46152
π : ι → Type ?u.46157
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y
exact (hz.resolve_left hx.symm).resolve_left hy.symm