x∈y∈z⇒x∈zは至る所で必要になるけど、よく見たらy∈z⇒y⊂zのことなんだから、ℕを定義したら初っ端に証明しとけばいいじゃん
これに何の問題があるのか