The operator A is not merely symmetric, but actually selfadjoint.
Actually, Theorem 3 gives more, namely,......
Actually, the proof gives an even more precise conclusion:......
Our present assumption implies that the last inequality in (8) must actually be an equality.
This accords with the intuition that as we pass down the coding tree, we find out more and more detailed information about the ordering actually represented.