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 )
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
s1 - s2 = w1 - w2 by EUCLID:73;
hence ( w1 <> w2 implies |.(w1 - w2).| > 0 ) by EUCLID:20; :: thesis: verum