Theorem

Let $\mathbf{A}$ be a $k\times k$ matrix of real elements. If $\mathbf{A}$ is symmetric and positive semidefinite then it has $k$ eigenvalues (counting multiplicities) and corresponding $k$ mutually orthogonal eigenvectors.