let N be Element of NAT ; :: thesis: for w being Point of (TOP-REAL N) st |.w.| = 0 holds
w = 0.REAL N
let w be Point of (TOP-REAL N); :: thesis: ( |.w.| = 0 implies w = 0.REAL N )
reconsider s = w as Element of REAL N by EUCLID:25;
assume |.w.| = 0 ; :: thesis: w = 0.REAL N
then s = 0.REAL N by EUCLID:11;
hence w = 0.REAL N ; :: thesis: verum