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