let p, q be Point of (TOP-REAL 2); :: thesis: dist p,q = dist (- p),(- q)
thus dist p,q = dist (q - q),(p - q) by Th23
.= dist (q - q),(p + (- q)) by EUCLID:45
.= dist |[0 ,0 ]|,(p + (- q)) by EUCLID:46, EUCLID:58
.= dist (p - p),(p + (- q)) by EUCLID:46, EUCLID:58
.= dist (p + (- p)),(p + (- q)) by EUCLID:45
.= dist (- p),(- q) by Th21 ; :: thesis: verum