Let $r\geq 3$. If the edges of $K_{r^2+1}$ are $r$-coloured then there exist $r+1$ vertices with at least one colour missing on the edges of the induced $K_{r+1}$.

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