let N be Element of 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 EUCLID:44 ; :: thesis: verum