Theorem: Line_comm (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
⊢ Line u v = Line v u
Tactic:
rw [Line, Line, Set.pair_comm]
State after:
no goals