>>684中の正則性公理
https://ja.wikipedia.org/wiki/%E6%AD%A3%E5%89%87%E6%80%A7%E5%85%AC%E7%90%86
の以下の2条件
「・∀xについて、∈がx上well-founded
　・∀xについて、無限下降列である x∋x_1∋x_2∋･･･ は存在しない。」
が同値であることは、単純に２項関係としての「∈」しか見てないから
これを「<」と置き換えても成り立つ
したがって、>>654の証明で全く十分であり、
「”∈を<としてよい”と書いてないから荒い」
とかいうのは読解力が欠如した🐎🦌の言い草である