let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds p, 0.REAL n are_orthogonal
let p be Point of (TOP-REAL n); :: thesis: p, 0.REAL n are_orthogonal
|(p,(0.REAL n))| = 0 by Th54;
hence p, 0.REAL n are_orthogonal by Def3; :: thesis: verum