| ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ ∀ x9 . x9 ⊆ x8 ⟶ atleastp 4 x9 ⟶ ∀ x10 : ο . (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ x10 |
|