let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds 0 <= |.p.|
let p be Point of (TOP-REAL n); :: thesis: 0 <= |.p.|
( |.p.| = sqrt |(p,p)| & 0 <= |(p,p)| ) by Th33, Th35;
hence 0 <= |.p.| by SQUARE_1:def 2; :: thesis: verum