let p, q be Point of (TOP-REAL 2); 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
; verum