Theorem: right_mem_Line (LeanCamCombi/SylvesterChvatal.lean)

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