simp [right_extend_mem_Line this]
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ {u, v, w} ⊆ Line u v
no goals