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