let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds
( |.p.| = 0 iff p = 0. (TOP-REAL n) )
let p be Point of (TOP-REAL n); :: thesis: ( |.p.| = 0 iff p = 0. (TOP-REAL n) )
n in NAT by ORDINAL1:def 13;
hence ( |.p.| = 0 iff p = 0. (TOP-REAL n) ) by Th61, TOPRNS_1:25; :: thesis: verum