∀ r ≥ 3, ∀ {V : Type} [inst : Fintype V] [DecidableEq V], Fintype.card V = r ^ 2 + 1 → ∀ (coloring : Sym2 V → Fin r), ∃ S k, S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k