Description: Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999) (New usage is discouraged.)