simp [h]
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∀ (x y z : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
h : b = c
⊢ c ∈ {a, b}
no goals