change Line a b ⊆ {a, b}
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ GenerateLine {a, b} ⊆ {a, b}
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ Line a b ⊆ {a, b}