let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )
let p be Point of (TOP-REAL n); :: thesis: ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )
( |(p,p)| = 0 implies p = 0. (TOP-REAL n) )

proof

assume |(p,p)| = 0 ; :: thesis: p = 0. (TOP-REAL n)
then ( n in NAT & |.p.| = 0 ) by Th38, ORDINAL1:def 12;
hence p = 0. (TOP-REAL n) by TOPRNS_1:24; :: thesis: verum

end;

hence ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) ) by Th30; :: thesis: verum