>>415
述語P(x)を「xはしっぽ同値類の代表選択関数」と定義。
選択公理から ∃xP(x) を推論でき、これと存在例化推論規則から P(c) を推論できる。名前cは証明内で自由に使ってよい。

>もし、『一意の基底の存在』だったら みんな困るよ （＾＾
だから分かってないと言われる。名前cを使ってよいのは証明内だけで証明外に染み出てはならない。つまり「みんなに一意」はど素人の誤解。

「存在しか言えないから実際には使えない」だの「存在しか言えないはずなのにみんなに一意はおかしい」だの言ってるサルは述語論理を初歩の初歩から分かってない。