let N be Element of NAT ; :: thesis: for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0
let w1, w2 be Point of (TOP-REAL N); :: thesis: ( w1 = w2 implies |.(w1 - w2).| = 0 )
assume w1 = w2 ; :: thesis: |.(w1 - w2).| = 0
then |.(w1 - w2).| = |.(0. (TOP-REAL N)).| by EUCLID:42
.= 0 by Th24 ;
hence |.(w1 - w2).| = 0 ; :: thesis: verum