let n be Nat; :: thesis: for p being Point of st ( for q being Point of holds p,q are_orthogonal ) holds
p = 0. (TOP-REAL n)
let p be Point of ; :: thesis: ( ( for q being Point of holds p,q are_orthogonal ) implies p = 0. (TOP-REAL n) )
assume for q being Point of 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