let X be RealUnitarySpace; :: thesis: for x, y being Point of X st x,y are_orthogonal holds
x, - y are_orthogonal
let x, y be Point of X; :: thesis: ( x,y are_orthogonal implies x, - y are_orthogonal )
assume x,y are_orthogonal ; :: thesis: x, - y are_orthogonal
then - (x .|. y) = - 0 ;
then x .|. (- y) = 0 by Th8;
hence x, - y are_orthogonal ; :: thesis: verum