strong_infinity_thm
• ∀ p • ∃ q • e p q ∧ (∀ x • e x q ⇒ (∃ y • e y q ∧ (∀ Z • ∃ z • e z y ∧ (∀ v • e v z ⇔ e v x ∧ Z v))) ∧ (∀ f • (∀ u• e u x ⇒ e (f u) q) ⇒ (∃ y • e y q ∧ (∀ u• e u x ⇒ e (f u) y))))
