let N be Nat; :: thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| = |.(w2 - w1).|
let w1, w2 be Point of (TOP-REAL N); :: thesis: |.(w1 - w2).| = |.(w2 - w1).|
thus |.(w1 - w2).| = |.(- (w1 - w2)).| by EUCLID:71
.= |.(w2 - w1).| by RLVECT_1:33 ; :: thesis: verum