Theorem: left_mem_Line (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w a b : V
⊢ a ∈ {a, b}
Tactic:
simp
State after:
no goals