The minimality condition in Definition 5.2 can be tricky to verify for a generic basis.Fortunately, in the case of an ONB, this condition is automatic.Proposition 5.10 If an orthonormal set of states of type A satisfies (5.2) for all pairs ofprocesses, then it must be minimal, and hence an ONB.