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