Exactly.
No, for the reality proof, you have the double assumption. For the orthogonality proof, you ONLY assume that the eigenvalues differ. Since eigenkets are, by definition, nonzero, proving orthogonality (which follows only from the Hermitian nature of the operator and the differing eigenvalues) will, in effect, prove that the eigenkets are not equal. But you're proving that. Assume as little as you need to, and prove as much as you can!So for orthonormality we also take the double assumption but in the sense the eigen values AND eigenkets are NOT equal
ie
are orthonormal
Cheers :-)