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:22;
thus |.(p1 - p2).| = |.q.|
.= |.(- q).| by EUCLID:10
.= |.(- (p1 - p2)).|
.= |.(p2 - p1).| by RLVECT_1:33 ; :: thesis: verum