| ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x1 . x1 ∈ u17 ⟶ Church17_p (x0 x1)) ⟶ (∀ x1 . x1 ∈ u17 ⟶ ∀ x2 . x2 ∈ u17 ⟶ x0 x1 = x0 x2 ⟶ x1 = x2) ⟶ ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x2 ∈ u17 ⟶ x3 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 (x0 x2) (x0 x3) = λ x5 x6 . x5) ⟶ ∀ x2 . x2 ⊆ u17 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4) |
|