可算選択公理で例えるなら、有限回の選択ならZFの中で可能だが、だからといって

「ゆえに、この作業を可算無限回繰り返せば、
　添え字の集合が可算無限でも選択関数が作れる
　(ZFの中で可算選択公理が公理ではなく定理として得られる)」

とは言えない。

ショルツにとっての Cor3.12 までの内容は、「有限回の選択ならZFの中で可能である」
に相当するものであり、そんなことは自明だったのだろう。ところが、Cor3.12 でいきなり
「ゆえに、この作業を可算無限回繰り返せば、添え字の集合が可算無限でも選択関数が作れる」
というステップが登場し、いや、それはおかしいと。
しかし、実際のIUTは「〇〇公理」と整備されているわけでもないので、
おかしい部分を正確に言語化することもできない。そんな感じだろう。