let n be Nat; :: thesis: for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) holds
p = 0. (TOP-REAL n)
let p be Point of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) implies p = 0. (TOP-REAL n) )
assume for q being Point of (TOP-REAL n) holds p,q are_orthogonal ; :: thesis: p = 0. (TOP-REAL n)
then p,p are_orthogonal ;
hence p = 0. (TOP-REAL n) by Th77; :: thesis: verum