Description: If two closed subspaces of a Hilbert space are orthogonal, their
subspace sum equals their subspace join. Lemma 3 of Kalmbach p. 67.
Note that the (countable) Axiom of Choice is used for this proof via
pjhth , although "the hard part" of this proof, chscl , requires no
choice. (Contributed by NM, 28-Oct-1999)(Revised by Mario Carneiro, 19-May-2014)(New usage is discouraged.)