>>425 補足

基礎の公理（正則性公理）
x ≠ Φ →∃y (y∈x ∧ ¬∃z(z ∈ x ∧ z ∈ y)).
　↓
”∈を、等号（=）を含まない、不等号＜と考える”
（∵ a ∈ a だめ、a ∈ b ∧ b ∈ a だめだから）
　↓
（無限降下列の禁止）
空でない集合x には∈ に関して極小となる元z ∈ x がある
（順序を先に言わないと、”極小”が言えないから）

を導くという流れかな
これが一番自然に感じるね