for G being finitely_colorable SimpleGraph
for C being finite Coloring of G
for c being set st c in C & card C = chromatic# G holds
ex v being Element of Vertices G st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of Vertices G st
( w in Adjacent v & w in d ) ) )