let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds |(p,p)| >= 0
let p be Point of (TOP-REAL n); :: thesis: |(p,p)| >= 0
reconsider f = p as FinSequence of REAL by EUCLID:27;
|(p,p)| = |(f,f)| ;
hence |(p,p)| >= 0 by RVSUM_1:149; :: thesis: verum