exact generateLine_close_middle ha hb hc
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw a c b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
no goals