Description: Define orthogonal complement of a subset (usually a subspace) of Hilbert
space. The orthogonal complement is the set of all vectors orthogonal
to all vectors in the subset. See ocval and chocvali for its value.
Textbooks usually denote this unary operation with the symbol _|_ as
a small superscript, although Mittelstaedt uses the symbol as a prefix
operation. Here we define a function (prefix operation) _|_ rather
than introducing a new syntactic form. This lets us take advantage of
the theorems about functions that we already have proved under set
theory. Definition of Mittelstaedt p. 9. (Contributed by NM, 7-Aug-2000)(New usage is discouraged.)