Parents |
gst-ax |
Children |
surreal |
Theorems |
strong_infinity_thm
|
⊢ ∃ e
• ∀ 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)))) |