| ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (x0 ∈ x2) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ⊆ x3 ⟶ x4 ∈ x2)) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x2) (∀ x6 . x6 ⊆ x3 ⟶ x6 ∈ x5) ⟶ x4) ⟶ x4)) (∀ x3 . x3 ⊆ x2 ⟶ or (∀ x4 : ο . (∀ x5 : ι → ι . bij x3 x2 x5 ⟶ x4) ⟶ x4) (x3 ∈ x2)) ⟶ x1) ⟶ x1 |
|