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)))
.= dist (|[0,0]|,(p + (- q))) by EUCLID:54, RLVECT_1:5
.= dist ((p - p),(p + (- q))) by EUCLID:54, RLVECT_1:5
.= dist ((p + (- p)),(p + (- q)))
.= dist ((- p),(- q)) by Th21 ; :: thesis: verum