>>507 補足
>間接的には 使っていてもおかしくないし
>IUTは 20世紀の膨大な代数学、代数幾何、数論幾何の蓄積の上にある
>そのどこかで 使っているのでは？ しらんけど （＾＾

そういえば、思い出してきたのが 集合の濃度の
ベルンシュタインの定理
選択公理を仮定すると いろいろ使えるらしい（下記）

あと、有理コーシー列と選択公理の関係
＜AI による概要＞
有理数のコーシー列（Cauchy sequence）と選択公理（Axiom of Choice）の主な関係は、実数の構成（完備化）における「可算選択公理」の必要性にあります
3. なぜ選択公理が必要か？
有理コーシー列で実数を定義しようとしても、適切に収束する列 {an} を作ることができない。
(引用終り)

そんなこんなで、実数の構成（完備化）だとか 関数だとか うんぬんかんぬん
あるいは、IUTのモノイドさんとか・・ 基礎的なところで
選択公理を使っていると思うよ しらんけど

(参考)
https://ja.wikipedia.org/wiki/%E6%BF%83%E5%BA%A6_(%E6%95%B0%E5%AD%A6)
濃度（のうど、英: cardinality カーディナリティ）とは、有限集合における「元の個数」を一般の集合に拡張したものである[1]。
集合の濃度は基数 (cardinal number) と呼ばれる数によって表される。歴史的には、カントールにより初めて無限集合のサイズが一つではないことが見出された[2][3]。

シュレーダー=ベルンシュタインの定理
選択公理を仮定すれば、任意の集合 X と Y に対して、X ≾ Y または Y ≾ X が成り立つ。

| X | = | Y | ⇔ X ≈ Y が常に成り立つ集合への数学的対象の割り当てを濃度といい、濃度として割り当てられる数学的対象を基数という（濃度 | X | は card(X), #X などとも表記される）。