The graph form is the two-colour case of the multicolour statement, and this module derives it that way rather than reproving it, so that the archive records the derivation.

Apply $Lax14.MulticolorRamsey.exists_monochromatic_set$ with two colours and requested size $max a b$, and colour a pair of vertices by $0$ when it is an edge of the graph and by $1$ otherwise. The colouring is well defined on unordered pairs because adjacency is symmetric, which is what $Sym2.lift$ requires. The resulting monochromatic set of size at least $max a b$ is a clique when its colour is $0$ and an independent set when its colour is $1$, since $Set.Pairwise$ in either case says exactly that distinct members are adjacent, respectively non-adjacent; $max$ then supplies the requested bound $a$ in the first branch and $b$ in the second.

Ramsey, On a problem of formal logic (Proc. London Math. Soc. 1930). The mathematical content sits in the proof of the multicolour statement ($Lax14Proofs.MulticolorRamsey$), ported from the proof package of the submission Monadic dependence and neighborhood complexity; this module is only the two-colour specialization.