let X be ComplexUnitarySpace; :: 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 by Def14;
then (- x) .|. (- y) = 0 by Th27;
hence - x, - y are_orthogonal by Def14; :: thesis: verum