>>317 追加
ちょっと思い出したので書く
ZFCの基礎公理において、下記の 尾畑研
補題3.14 x∈yとy∈xを同時に満たす集合x,yは存在しない
定理3.17 x1∋x2∋・・・∋xn∋・・・ を満たすもの(無限下降列という)は存在しない
が、背理法を使っていたことを思い出したので書くね

これを、ザコボスのチャレンジ問題として投下するよ
この二つの 背理法を使わない証明は どうよ？ｗｗ　（＾＾

(参考)
https://www.math.is.tohoku.ac.jp/~obata/student/subject/
東北大 尾畑研
「集合・写像・数の体系　数学リテラシーとして」の草稿(pdf)
https://www.math.is.tohoku.ac.jp/~obata/student/subject/TaikeiBook/Taikei-Book_03.pdf
TAIKEI-BOOK : 2019/1/1(22:21)
第3章 集合の演算
3.3集合の公理
ZF公理系
P48
(S9)基礎の公理 空でない集合Aにはすべてのy∈Aに対してy∉xを満たすx∈Aが存在する(このようなxを∈に関するの極小元という)

基礎の公理S9の役割を見ておこう
補題3.14 x∈yとy∈xを同時に満たす集合x,yは存在しない
証明：（背理法を使っているが 略す）

定理3.17 集合の元の列 x1,x2,・・・,xn,・・・で
　x1∋x2∋・・・∋xn∋・・・
を満たすもの(無限下降列という)は存在しない
証明 集合A＝{xn | n∈N} が基礎の公理に反する 4)
4)置換公理によって写像の像集合は確かに集合になる。このことからAは集合である
（注：背理法証明だが、詳細は書かれていない。下記 (google検索)ご参照）

(google検索)
基礎の公理で 無限下降列が存在しないことの 証明
AI による概要
基礎の公理（正則性公理）により、いかなる集合においても
∈ に関する無限下降列 x_0 ∋ x_1 ∋ x_2 ・・・ （すなわち、x_n+1 ∈ x_n となるような集合の無限列）は存在しません。これは背理法と選択公理を用いて次のように証明されます
略す