 By a complicated passage through formal theories for choice sequences it was known that the theory \(\bID_{1}\) can be reduced to \(\bID_{1}^{i}(\cO)\). The first ordinal analysis for the theory \(\bID_{1}^{i}(\cO)\) was obtained by Howard (1972). Via the known proof-theoretical reductions this entailed also an ordinal analysis for \(\bID_{1}\). The proof-theoretic ordinal of \(\bID_{1}\) is the Bachmann-Howard ordinal, which is denoted by \({\psi_{\sOmega_{1}}(\varepsilon_{\Omega_1+1})}\) in the system of  Definition 5.11.