>>172
>証明のどこで選択公理使ってると？　具体的な箇所を示して。

すでに述べた
　>>167より
『コーシー列に二種類 あることを認めようね
　一つは、構成可能なコーシー列 （例えば オイラー数 (Euler's number)e =1+1+1/2!+1/3!+・・ https://en.wikipedia.org/wiki/E_(mathematical_constant)）
　もう一つは、非構成可能なコーシー列
　非構成可能なコーシー列の存在を示すのに、(可算)選択公理を使う
　非構成可能なコーシー列の存在を示せないと 完備がいえない』

なお、下記が参考になるだろう
選択公理の能力は、出力できる非構成可能な列の長さで測れる
可算選択公理は実はDC(ω)と同値
任意の順序数 αについて DC(ℵα)⟺AC（フルパワー選択公理）

(参考)
https://ja.wikipedia.org/wiki/%E5%BE%93%E5%B1%9E%E9%81%B8%E6%8A%9E%E5%85%AC%E7%90%86
従属選択公理(英語: axiom of dependent choice; DCと略される)とは、選択公理(AC)の弱い形で、しかし実解析の大部分を行うのに十分な公理である。これはパウル・ベルナイスによって1942年の、解析学を実行するのに必要な集合論的公理を検討する逆数学の論文で導入された

従属選択公理とは、次の言明である
略
実のところ、x0 は X の好きな元を選ぶことができる。(これを見るには、x0 から始められる
R の有限鎖全体を考え、その中に右が左の延長であるという二項関係を考えてそこに従属選択公理を適用すれば有限鎖の無限列ができるので、それの和を取ればよい。)

使用例
このような公理が無いとしても、各 n について普通の帰納法によって最初の n 項を有限列としてとることはできる。従属選択公理が主張しているのは、その極限であるような可算無限列が取れるということである。

公理 DC はACの断片であって、超限帰納法の各ステップで選択をする必要があって、それまでの選択に独立した選択ができない場合に、可算長の列を構成するのに必要である。

従属選択公理の一般化としてさらに長い超限列の生成を認めるものを考えることができる
公理
DC(ℵα)
略す

この記法を採用すると、可算選択公理は実はDC(ω)と同値であり、実際に一般化になっていることがわかり、全ての順序数について上の命題が成立すると仮定すると選択公理が導ける[1]。

定理(ZF) ― 「任意の順序数 αについて DC(ℵα)⟺AC