| ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . infinite x2 ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ⊆ x2 ⟶ equip x4 x1 ⟶ x3 x4 ∈ x0) ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (∀ x6 : ο . (∀ x7 . and (x7 ∈ x0) (and (infinite x5) (∀ x8 . x8 ⊆ x5 ⟶ equip x8 x1 ⟶ x3 x8 = x7)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 |
|