let p1, p2 be Point of (TOP-REAL 2); :: thesis: |.(p1 - p2).| = |.(p2 - p1).|
thus |.(p1 - p2).| = |.(- (p1 - p2)).| by EUCLID:13
.= |.(p2 - p1).| by EUCLID:48 ; :: thesis: verum