exact ((h' z (middle_extend_mem_Line h)).2.1 h).elim
case refine_2.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x z y
⊢ z ∈ {x, y}
no goals