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) )

( |(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

hence
( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )
by Th30; :: thesis: verum
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;then ( n in NAT & |.p.| = 0 ) by Th38, ORDINAL1:def 12;

hence p = 0. (TOP-REAL n) by TOPRNS_1:24; :: thesis: verum