have ⟨b, h⟩ := exists_ne a
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a : V
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : b ≠ a
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L